# HG changeset patch
# User wenzelm
# Date 1727460768 -7200
# Node ID dfbe65315fc956375f3f81004fb476d4e4cc6ddc
# Parent  d76230f575f2b2499432c69dd1a88e5407430404
unused (see 7c1e73540990);

diff -r d76230f575f2 -r dfbe65315fc9 src/Pure/Syntax/parser.ML
--- 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)])