--- a/src/Pure/Syntax/parser.ML Mon Sep 23 10:45:05 2024 +0200
+++ b/src/Pure/Syntax/parser.ML Mon Sep 23 10:56:25 2024 +0200
@@ -630,19 +630,15 @@
(S :: Si,
if Lexicon.tokens_match_ord (a, c) = EQUAL then movedot_term c S :: Sii else Sii)
| (A, prec, ts, [], id, j) => (*completer operation*)
- let val tt = if id = "" then ts else [Node (id, rev ts)] in
- if j = i then (*lambda production?*)
- let
- val (prec', used') = update_trees (A, (tt, prec)) used;
- val Slist = getS A prec prec' Si;
- val States' = map (movedot_nonterm tt) Slist;
- in processS used' (States' @ States) (S :: Si, Sii) end
- else
- let
- val Slist = get_states Estate j A prec;
- val States' = map (movedot_nonterm tt) Slist;
- in processS used (States' @ States) (S :: Si, Sii) end
- end)
+ let
+ val tt = if id = "" then ts else [Node (id, rev ts)];
+ val (used', Slist) =
+ if j = i then (*lambda production?*)
+ let val (prec', used') = update_trees (A, (tt, prec)) used
+ in (used', getS A prec prec' Si) end
+ else (used, get_states Estate j A prec);
+ val States' = map (movedot_nonterm tt) Slist;
+ in processS used' (States' @ States) (S :: Si, Sii) end)
in processS Inttab.empty states ([], []) end;