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