tuned;
authorwenzelm
Mon, 23 Sep 2024 10:45:05 +0200
changeset 80927 81b942537dd1
parent 80926 eabc517e7413
child 80928 c6ce90275c3d
tuned;
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;