# HG changeset patch
# User wenzelm
# Date 1727461778 -7200
# Node ID a9782ba039fb7a71fd72403d3a42ae9329eac138
# Parent  a5ce1be6c46504608bf4b4e96a96cf6199a25315
unused (see 954e9d6782ea);

diff -r a5ce1be6c465 -r a9782ba039fb src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Fri Sep 27 20:19:38 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Fri Sep 27 20:29:38 2024 +0200
@@ -16,7 +16,6 @@
     Tip of Lexicon.token
   val pretty_parsetree: parsetree -> Pretty.T list
   val parse: gram -> string -> Lexicon.token list -> parsetree list
-  val branching_level: int Config.T
 end;
 
 structure Parser: PARSER =
@@ -535,11 +534,6 @@
   symb list *       (*input: rest of rhs*)
   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