fix #1353

HOL-Theorem-Prover · Nov 28, 2024 · a166853 · a166853
1 parent 998d07f
commit a166853
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/tools/Holmake/HolParser.sml b/tools/Holmake/HolParser.sml
@@ -27,7 +27,7 @@ in
       comdepth = ref 0, comstart = ref NONE, pardepth = ref 0, parseError = parseError})
     val lookahead = ref NONE
     fun go () =
-      case (case !lookahead of SOME tk => tk | NONE => lex ()) of
+      case (case !lookahead of SOME tk => (lookahead := NONE; tk) | NONE => lex ()) of
         H.Decl (td, look) => (lookahead := look; TopDecl td)
       | H.CloseParen p => (parseError (p, p + 1) ("unexpected ')'"); go ())
       | H.EndTok _ => go ()