diff -r 9e2eb05cc2b7 -r faccef6c0806 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Sat Oct 05 22:24:24 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Sat Oct 05 22:46:21 2024 +0200
@@ -661,14 +661,11 @@
 fun update_prec (A, p) used =
   Inttab.map_default (A, init_prec) (fn (_, output) => (p, output)) used;
 
-fun get_states A min max =
-  let
-    fun ok (Nonterminal (B, p) :: _) = A = B andalso upto_prec min max p
-      | ok _ = false;
-  in filter (fn (_, ss, _): state => ok ss) end;
-
-fun movedot_nonterm out' (info, Nonterminal _ :: sa, out) : state =
-  (info, sa, append_output out' out);
+fun movedot_states out' A min max = map_filter
+  (fn ((info, Nonterminal (B, p) :: sa, out): state) =>
+      if A = B andalso upto_prec min max p then SOME (info, sa, append_output out' out)
+      else NONE
+    | _ => NONE);
 
 fun process_states (Gram {prods = gram_prods, chains = gram_chains, ...}) stateset i c states0 =
   let
@@ -722,12 +719,11 @@
               let
                 val (A, p, id, j) = info;
                 val out' = node_output {nonterm = A, const = id} out;
-                val (used', Slist) =
+                val (used', states') =
                   if j = i then (*lambda production?*)
                     let val (q, used') = update_output (A, (out', p)) used
-                    in (used', get_states A q p Si) end
-                  else (used, get_states A no_prec p (get j));
-                val states' = map (movedot_nonterm out') Slist;
+                    in (used', movedot_states out' A q p Si) end
+                  else (used, movedot_states out' A no_prec p (get j));
               in process used' (states' @ states) (S :: Si, Sii) end)
 
     val (Si, Sii) = process Inttab.empty states0 ([], []);