--- a/src/Pure/Syntax/parser.ML Fri Sep 27 20:09:54 2024 +0200
+++ b/src/Pure/Syntax/parser.ML Fri Sep 27 20:12:48 2024 +0200
@@ -536,13 +536,6 @@
parsetree list; (*output (reversed): already parsed nonterminals on rhs*)
-(*Get all rhss with precedence >= min_prec*)
-fun get_RHS min_prec = filter (fn (_, _, prec: int) => prec >= min_prec);
-
-(*Get all rhss with precedence >= min_prec and < max_prec*)
-fun get_RHS' min_prec max_prec =
- filter (fn (_, _, prec: int) => prec >= min_prec andalso prec < max_prec);
-
(*Add parse tree to list and eliminate duplicates
saving the maximum precedence*)
fun conc (t: parsetree list, prec: int) [] = (NONE, [(t, prec)])