diff -r b4056a71eca2 -r b54d51df9065 src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Mon Aug 21 18:03:12 1995 +0200
+++ b/src/Pure/Thy/thy_read.ML	Wed Aug 30 14:04:39 1995 +0200
@@ -501,13 +501,15 @@
   let
     val (thy_name, ThyInfo {path, children, thy_time, ml_time, theory, thms}) =
       thyinfo_of_sign (#sign (rep_thm thm));
+
     val thms' = Symtab.update_new ((name, thm), thms)
       handle Symtab.DUPLICATE s => 
         (if eq_thm (the (Symtab.lookup (thms, name)), thm) then 
-           (writeln ("Warning: Theorem database already contains copy of\
+           (writeln ("Warning: Theory database already contains copy of\
                      \ theorem " ^ quote name);
             thms)
-         else error ("Duplicate theorem name " ^ quote s));
+         else error ("Duplicate theorem name " ^ quote s
+                     ^ " used in theory database"));
   in
     loaded_thys := Symtab.update
      ((thy_name, ThyInfo {path = path, children = children,