# HG changeset patch
# User clasohm
# Date 786974703 -3600
# Node ID ea19f22ed23c0ad05282afc1ae784e1205ada7f0
# Parent  9f8bcf1a4cff7939227a52184124a90366e1ab2b
added warning for already stored theorem to store_thm

diff -r 9f8bcf1a4cff -r ea19f22ed23c src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Thu Dec 08 16:42:58 1994 +0100
+++ b/src/Pure/Thy/thy_read.ML	Fri Dec 09 13:05:03 1994 +0100
@@ -478,7 +478,12 @@
     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 => error ("Duplicate theorem name " ^ quote s);
+      handle Symtab.DUPLICATE s => 
+        (if eq_thm (the (Symtab.lookup (thms, name)), thm) then 
+           (writeln ("Warning: Theorem database already contains copy of\
+                     \ theorem " ^ quote name);
+            thms)
+         else error ("Duplicate theorem name " ^ quote s));
   in
     loaded_thys := Symtab.update
      ((thy_name, ThyInfo {path = path, children = children,