tuned;

--- a/src/Pure/Syntax/parser.ML	Sat Sep 28 15:58:09 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Sat Sep 28 16:07:46 2024 +0200
@@ -588,14 +588,12 @@
 
 fun process_states (Gram {prods = gram_prods, chains = gram_chains, ...}) stateset i c states0 =
   let
-    (*get all productions of a NT and NTs chained to it which can
-      be started by specified token*)
-    fun add_prods i tok nt ok =
+    fun add_prods nt min max =
       let
         fun add (rhs, id, prod_prec) =
-          if ok prod_prec then cons ((nt, prod_prec, id, i), rhs, []) else I;
+          if until_prec min max prod_prec then cons ((nt, prod_prec, id, i), rhs, []) else I;
         fun token_prods prods =
-          fold add (prods_lookup prods tok) #>
+          fold add (prods_lookup prods c) #>
           fold add (prods_lookup prods Lexicon.dummy);
         val nt_prods = #2 o Vector.nth gram_prods;
       in fold (token_prods o nt_prods) (chains_all_preds gram_chains [nt]) end;
@@ -615,11 +613,11 @@
                         (used, Parsetrees.fold movedot_lambda used_trees states)
                       else (*wanted precedence hasn't been parsed yet*)
                         let
-                          val states' = states |> add_prods i c nt (until_prec min_prec used_prec)
+                          val states' = states |> add_prods nt min_prec used_prec
                             |> Parsetrees.fold movedot_lambda used_trees;
                         in (update_prec (nt, min_prec) used, states') end
                   | NONE => (*nonterminal is parsed for the first time*)
-                      let val states' = states |> add_prods i c nt (until_prec min_prec no_prec);
+                      let val states' = states |> add_prods nt min_prec no_prec;
                       in (Inttab.update (nt, (min_prec, Parsetrees.empty)) used, states') end);
               in process used' states' (S :: Si, Sii) end
           | Terminal a :: sa => (*scanner operation*)