diff -r a2ad1c166ac8 -r d2d1138e0ddc src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun Jul 08 19:51:55 2007 +0200
+++ b/src/Pure/theory.ML	Sun Jul 08 19:51:58 2007 +0200
@@ -96,8 +96,8 @@
 fun make_thy (axioms, defs, oracles) =
   Thy {axioms = axioms, defs = defs, oracles = oracles};
 
-fun err_dup_axms dups = error ("Duplicate axiom(s): " ^ commas_quote dups);
-fun err_dup_oras dups = error ("Duplicate oracle(s): " ^ commas_quote dups);
+fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
+fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
 
 structure ThyData = TheoryDataFun
 (
@@ -115,7 +115,7 @@
       val axioms = NameSpace.empty_table;
       val defs = Defs.merge pp (defs1, defs2);
       val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
-        handle Symtab.DUPS dups => err_dup_oras dups;
+        handle Symtab.DUP dup => err_dup_ora dup;
     in make_thy (axioms, defs, oracles) end;
 );
 
@@ -182,7 +182,7 @@
   let
     val axms = map (apsnd (Compress.term thy o Logic.varify) o prep_axm thy) raw_axms;
     val axioms' = NameSpace.extend_table (Sign.naming_of thy) axms axioms
-      handle Symtab.DUPS dups => err_dup_axms dups;
+      handle Symtab.DUP dup => err_dup_axm dup;
   in axioms' end);
 
 in
@@ -307,7 +307,7 @@
 
 fun add_oracle (bname, oracle) thy = thy |> map_oracles (fn oracles =>
   NameSpace.extend_table (Sign.naming_of thy) [(bname, (oracle, stamp ()))] oracles
-    handle Symtab.DUPS dups => err_dup_oras dups);
+    handle Symtab.DUP dup => err_dup_ora dup);
 
 end;