# HG changeset patch
# User wenzelm
# Date 1164560855 -3600
# Node ID f119c730f5093b7c4d0c858d88606a6a0a5761e6
# Parent  07f8cd0d79625a286eb270d6da6fca32ba014854
extend_trtab: allow identical trfuns to be overwritten;

diff -r 07f8cd0d7962 -r f119c730f509 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Nov 26 18:07:34 2006 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sun Nov 26 18:07:35 2006 +0100
@@ -94,11 +94,11 @@
 fun err_dup_trfuns name cs =
   error ("More than one " ^ name ^ " for " ^ commas_quote cs);
 
-fun extend_trtab name trfuns tab = Symtab.extend (tab, trfuns)
+fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns;
+
+fun extend_trtab name trfuns tab = Symtab.extend (remove_trtab trfuns tab, trfuns)
   handle Symtab.DUPS cs => err_dup_trfuns name cs;
 
-fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns;
-
 fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2)
   handle Symtab.DUPS cs => err_dup_trfuns name cs;