# HG changeset patch
# User wenzelm
# Date 1517340115 -3600
# Node ID f686e756badbcb70dbe8bb9469955c36de2cdf23
# Parent  e8b2d85e4a8b62dee2148f5455f573c32448e59e
unused;

diff -r e8b2d85e4a8b -r f686e756badb src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Tue Jan 30 20:20:46 2018 +0100
+++ b/src/Pure/Syntax/parser.ML	Tue Jan 30 20:21:55 2018 +0100
@@ -79,7 +79,6 @@
 type prods = (symb list * string * int) list Tokens.table;  (*start_token ~> [(rhs, name, prio)]*)
 
 val prods_empty: prods = Tokens.empty;
-val prods_merge: prods * prods -> prods = Tokens.merge (op =);
 fun prods_lookup (prods: prods) = Tokens.lookup_list prods;
 fun prods_update entry : prods -> prods = Tokens.update entry;
 fun prods_content (prods: prods) = distinct (op =) (maps #2 (Tokens.dest prods));