# HG changeset patch
# User clasohm
# Date 814624905 -3600
# Node ID 396ef8aa37b74b0f37ef7e9b02ca30215888db75
# Parent  63a5788774f7b94abd4e12deec31fcb741118c93
removed "duplicate" warning from store_thm_db;
changed place where store_thm_db is called for a theory's axioms

diff -r 63a5788774f7 -r 396ef8aa37b7 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Wed Oct 25 12:53:53 1995 +0100
+++ b/src/Pure/Thy/thm_database.ML	Wed Oct 25 13:41:45 1995 +0100
@@ -80,10 +80,7 @@
                 else case find_first (fn (_, (n, _)) => n = name) old_thms of
                        Some (_, (_, t)) => eq_thm (t, thm)
                      | None => false
-            in if duplicate then
-                 (writeln ("Warning: Theorem database already contains copy of\
-                           \ theorem " ^ quote name);
-                  None)
+            in if duplicate then None
                else update_db true
                       cs (Symtab.update ((c, tagged_thm :: old_thms), result))
             end;
diff -r 63a5788774f7 -r 396ef8aa37b7 src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Wed Oct 25 12:53:53 1995 +0100
+++ b/src/Pure/Thy/thy_read.ML	Wed Oct 25 13:41:45 1995 +0100
@@ -627,6 +627,17 @@
           use (out_name tname);
           save_thy_ss ();
 
+          (*Store axioms of theory
+            (but only if it's not a copy of an older theory)*)
+          let val parents = parents_of tname;
+              val this_thy = theory_of tname;
+              val axioms =
+                if length parents = 1
+                   andalso Sign.eq_sg (sign_of (theory_of (hd parents)),
+                                       sign_of this_thy) then []
+                else axioms_of this_thy;
+          in map store_thm_db axioms end;
+
           if not (!delete_tmpfiles) then ()
           else delete_file (out_name tname);
 
@@ -646,17 +657,6 @@
        use_string
          ["val _ = store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"];
 
-       (*Store axioms of theory
-         (but only if it's not a copy of an older theory)*)
-       let val parents = parents_of tname;
-           val this_thy = theory_of tname;
-           val axioms =
-             if length parents = 1
-                andalso Sign.eq_sg (sign_of (theory_of (hd parents)),
-                                    sign_of this_thy) then []
-             else axioms_of this_thy;
-       in map store_thm_db axioms end;
-
        (*Add theory to list of all loaded theories (for 00-chart.html)
          and add it to its parents' sub-charts*)
        if !make_html then