src/Pure/Thy/thy_read.ML

 (*Store a theorem in the thy_info of its theory*)
 fun store_thm (name, thm) =
   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,
        thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms'}),
       ! loaded_thys);