# HG changeset patch
# User wenzelm
# Date 1727469360 -7200
# Node ID a594b5e922add28ab2cb419f1926f8e83fcf6243
# Parent  54f5d6e1c317bfca0fbb04ac7678c8b1987b0deb
tuned signature;

diff -r 54f5d6e1c317 -r a594b5e922ad src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Fri Sep 27 22:28:46 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Fri Sep 27 22:36:00 2024 +0200
@@ -591,7 +591,7 @@
 
 fun movedot_nonterm tt (info, Nonterminal _ :: sa, ts) : state = (info, sa, tt @ ts);
 
-fun process_states (Gram {prods = gram_prods, chains = gram_chains, ...}) stateset i c states =
+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*)
@@ -606,27 +606,27 @@
       in fold (token_prods o nt_prods) (chains_all_preds gram_chains [nt]) end;
 
     fun process _ [] (Si, Sii) = (Si, Sii)
-      | process used ((S as (info, symbs, ts)) :: States) (Si, Sii) =
+      | process used ((S as (info, symbs, ts)) :: states) (Si, Sii) =
           (case symbs of
-            Markup (_, body) :: sa => process used ((info, body @ sa, ts) :: States) (Si, Sii)
+            Markup (_, body) :: sa => process used ((info, body @ sa, ts) :: states) (Si, Sii)
           | Nonterminal (nt, min_prec) :: sa =>
               let (*predictor operation*)
                 fun movedot_lambda (t, k) = min_prec <= k ? cons (info, sa, t @ ts)
-                val (used', States') =
+                val (used', states') =
                   (case Inttab.lookup used nt of
                     SOME (used_prec, used_trees) => (*nonterminal has been processed*)
                       if used_prec <= min_prec then
                         (*wanted precedence has been processed*)
-                        (used, Parsetrees.fold movedot_lambda used_trees States)
+                        (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 i c nt (until_prec min_prec used_prec)
                             |> Parsetrees.fold movedot_lambda used_trees;
-                        in (update_prec (nt, min_prec) used, States') end
+                        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);
-                      in (Inttab.update (nt, (min_prec, Parsetrees.empty)) used, States') end);
-              in process used' States' (S :: Si, Sii) end
+                      let val states' = states |> add_prods i c nt (until_prec 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*)
               let
                 val (_, _, id, _) = info;
@@ -635,7 +635,7 @@
                   else (*move dot*)
                     let val ts' = if Lexicon.valued_token c orelse id <> "" then Tip c :: ts else ts
                     in (info, sa, ts') :: Sii end;
-              in process used States (S :: Si, Sii') end
+              in process used states (S :: Si, Sii') end
           | [] => (*completer operation*)
               let
                 val (A, p, id, j) = info;
@@ -645,10 +645,10 @@
                     let val (q, used') = update_trees (A, (tt, p)) used
                     in (used', get_states_lambda A q p Si) end
                   else (used, get_states A p (Array.nth stateset j));
-                val States' = map (movedot_nonterm tt) Slist;
-              in process used' (States' @ States) (S :: Si, Sii) end)
+                val states' = map (movedot_nonterm tt) Slist;
+              in process used' (states' @ states) (S :: Si, Sii) end)
 
-    val (Si, Sii) = process Inttab.empty states ([], []);
+    val (Si, Sii) = process Inttab.empty states0 ([], []);
   in
     Array.upd stateset i Si;
     Array.upd stateset (i + 1) Sii