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

diff -r eabc517e7413 -r 81b942537dd1 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Sun Sep 22 18:47:43 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Mon Sep 23 10:45:05 2024 +0200
@@ -638,8 +638,10 @@
                     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
-                  in processS used (map (movedot_nonterm tt) Slist @ States) (S :: Si, Sii) end
+                  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)
   in processS Inttab.empty states ([], []) end;