extend_trtab: allow identical trfuns to be overwritten;

--- 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;