diff -r a2ad1c166ac8 -r d2d1138e0ddc src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Jul 08 19:51:55 2007 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Jul 08 19:51:58 2007 +0200
@@ -98,16 +98,16 @@
 
 fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
 
-fun err_dup_trfuns name cs =
-  error ("More than one " ^ name ^ " for " ^ commas_quote cs);
+fun err_dup_trfun name c =
+  error ("More than one " ^ name ^ " for " ^ quote c);
 
 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;
+  handle Symtab.DUP c => err_dup_trfun name c;
 
 fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2)
-  handle Symtab.DUPS cs => err_dup_trfuns name cs;
+  handle Symtab.DUP c => err_dup_trfun name c;
 
 
 (* print (ast) translations *)