unused (see 954e9d6782ea);
authorwenzelm
Fri, 27 Sep 2024 20:29:38 +0200
changeset 80977 a9782ba039fb
parent 80976 a5ce1be6c465
child 80978 5e2b1588c5cb
unused (see 954e9d6782ea);
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