diff -r bbad381bc89a -r 584828fa7a97 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Tue Sep 24 20:10:11 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Tue Sep 24 21:24:44 2024 +0200
@@ -525,10 +525,6 @@
 fun get_RHS' min_prec max_prec =
   filter (fn (_, _, prec: int) => prec >= min_prec andalso prec < max_prec);
 
-(*Make states using a list of rhss*)
-fun mk_states i lhs_ID =
-  map (fn (rhs, id, prod_prec) => ((lhs_ID, prod_prec, id, i), rhs, []));
-
 (*Add parse tree to list and eliminate duplicates
   saving the maximum precedence*)
 fun conc (t: parsetree list, prec: int) [] = (NONE, [(t, prec)])
@@ -593,26 +589,26 @@
           (case S of
             (info, Nonterminal (nt, min_prec) :: sa, ts) =>
               let (*predictor operation*)
+                fun mk_state (rhs, id, prod_prec) = ((nt, prod_prec, id, i), rhs, []);
+                fun movedot_lambda (t, k) = if min_prec <= k then SOME (info, sa, t @ ts) else NONE;
                 val (used', new_states) =
                   (case Inttab.lookup used nt of
                     SOME (used_prec, l) => (*nonterminal has been processed*)
                       if used_prec <= min_prec then
                         (*wanted precedence has been processed*)
-                        (used, movedot_lambda min_prec (info, sa, ts) l)
+                        (used, map_filter movedot_lambda l)
                       else (*wanted precedence hasn't been parsed yet*)
                         let
                           val tk_prods = prods_for gram c nt;
-                          val States2 = mk_states i nt (get_RHS' min_prec used_prec tk_prods);
-                          val States1 = movedot_lambda min_prec (info, sa, ts) l;
+                          val States2 = map mk_state (get_RHS' min_prec used_prec tk_prods);
+                          val States1 = map_filter movedot_lambda l;
                         in (update_prec (nt, min_prec) used, States1 @ States2) end
                   | NONE => (*nonterminal is parsed for the first time*)
                       let
                         val tk_prods = prods_for gram c nt;
-                        val States' = mk_states i nt (get_RHS min_prec tk_prods);
+                        val States' = map mk_state (get_RHS min_prec tk_prods);
                       in (Inttab.update (nt, (min_prec, [])) used, States') end);
-              in
-                process used' (new_states @ States) (S :: Si, Sii)
-              end
+              in process used' (new_states @ States) (S :: Si, Sii) end
           | (info as (_, _, id, _), Terminal a :: sa, ts) => (*scanner operation*)
               let
                 val Sii' =