# HG changeset patch
# User wenzelm
# Date 1727081785 -7200
# Node ID c6ce90275c3d0cb4c074f76d5ef5ed25efc4b995
# Parent  81b942537dd1f16830c924174ac4abd5ea838086
tuned;

diff -r 81b942537dd1 -r c6ce90275c3d src/Pure/Syntax/parser.ML
--- 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;