diff -r dfbe65315fc9 -r a5ce1be6c465 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Fri Sep 27 20:12:48 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Fri Sep 27 20:19:38 2024 +0200
@@ -536,6 +536,12 @@
   parsetree list;   (*output (reversed): already parsed nonterminals on rhs*)
 
 
+(*trigger value for warnings*)
+val branching_level = Config.declare_int ("syntax_branching_level", \<^here>) (K 600);
+
+
+local
+
 (*Add parse tree to list and eliminate duplicates
   saving the maximum precedence*)
 fun conc (t: parsetree list, prec: int) [] = (NONE, [(t, prec)])
@@ -578,16 +584,8 @@
 fun get_states A max_prec =
   filter (head_nonterm (fn (B, p) => A = B andalso p <= max_prec));
 
-
 fun movedot_nonterm tt (info, Nonterminal _ :: sa, ts) : state = (info, sa, tt @ ts);
 
-
-(*trigger value for warnings*)
-val branching_level = Config.declare_int ("syntax_branching_level", \<^here>) (K 600);
-
-
-local
-
 fun process_states (Gram {prods = gram_prods, chains = gram_chains, ...}) stateset i c states =
   let
     (*get all productions of a NT and NTs chained to it which can