# HG changeset patch
# User clasohm
# Date 809784279 -7200
# Node ID b54d51df90657f3984d660f28f7661ef42f7e196
# Parent  b4056a71eca2983ca7e7d4e55b7048728ba845fa
added check for duplicate theorems in theorem database;
changed warnings and error messages in thy_read to distinguish between
theorems in theor_y_ database and in theor_em_ database

diff -r b4056a71eca2 -r b54d51df9065 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Mon Aug 21 18:03:12 1995 +0200
+++ b/src/Pure/Thy/thm_database.ML	Wed Aug 30 14:04:39 1995 +0200
@@ -48,8 +48,8 @@
   in distinct (consts t) end;
 
 (*store a theorem in database*)
-fun store_thm_db (named_thm as (name, t)) =
-  let val {prop, hyps, ...} = rep_thm t;
+fun store_thm_db (named_thm as (name, thm)) =
+  let val {prop, hyps, ...} = rep_thm thm;
 
       val consts = distinct (flat (map list_consts (prop :: hyps)));
 
@@ -57,18 +57,33 @@
 
       val tagged_thm = (num + 1, named_thm);
 
-      fun update_db [] result = result
-        | update_db (c :: cs) result =
-            let val old_thms = Symtab.lookup_multi (result, c);
-            in update_db cs (Symtab.update ((c, tagged_thm :: old_thms),
-                                            result))
+      fun update_db _ [] result = result
+        | update_db warned (c :: cs) result =
+            let
+              val old_thms = Symtab.lookup_multi (result, c);
+
+              val warned' =
+                case find_first (fn (_, (n, _)) => n = name) old_thms of
+                    Some (_, (_, t)) =>
+                      if eq_thm (t, thm) then
+                        (if not warned then
+                           writeln ("Warning: Theorem database already \
+                                    \contains copy of theorem " ^ quote name)
+                         else ();
+                         true)
+                     else error ("Duplicate theorem name " ^ quote name
+                                 ^ " used in theorem database")
+                 | None => warned;
+            in update_db warned' cs
+                 (if warned' then result
+                  else (Symtab.update ((c, tagged_thm :: old_thms), result)))
             end;
   in if consts = [] then writeln ("Warning: Theorem " ^ name ^
                                   " cannot be stored in ThmDB\n\t because it \
                                   \contains no or only ignored constants.")
                     else ();
-     thm_db := (num+1, update_db consts db);
-     t
+     thm_db := (num+1, update_db false consts db);
+     thm
   end;
 
 (*intersection of two descending theorem lists*)
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,