# HG changeset patch
# User clasohm
# Date 809958352 -7200
# Node ID 934183dfc7868a86e615f941dd9938398f58f45f
# Parent  3d408455d69f2acf11aee3cef4526d2e2585d61c
fixed bug: duplicate "duplicate" warnings

diff -r 3d408455d69f -r 934183dfc786 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Fri Sep 01 13:51:49 1995 +0200
+++ b/src/Pure/Thy/thm_database.ML	Fri Sep 01 14:25:52 1995 +0200
@@ -57,21 +57,23 @@
 
       val tagged_thm = (num + 1, named_thm);
 
-      fun update_db [] result = result
-        | update_db (c :: cs) result =
+      fun update_db warned [] result = result
+        | update_db warned (c :: cs) result =
             let
               val old_thms = Symtab.lookup_multi (result, c);
 
-              val duplicate =
+              val (duplicate, warned') =
                 case find_first (fn (_, (n, _)) => n = name) old_thms of
                     Some (_, (_, t)) =>
-                      if same_thm (t, thm) then true
+                      if same_thm (t, thm) then (true, warned)
                       else
-                        (writeln ("Warning: Duplicate theorem name "
-                                  ^ quote name ^ " used in theorem database");
-                         false)
-                 | None => false;
-            in update_db cs
+                        (if not warned then
+                           writeln ("Warning: Duplicate theorem name " ^
+                                    quote name ^ " used in theorem database")
+                         else ();
+                         (false, true))
+                 | None => (false, warned);
+            in update_db warned' cs
                  (if duplicate then result
                   else (Symtab.update ((c, tagged_thm :: old_thms), result)))
             end;
@@ -79,7 +81,7 @@
                                   " cannot be stored in ThmDB\n\t because it \
                                   \contains no or only ignored constants.")
                     else ();
-     thm_db := (num+1, update_db consts db);
+     thm_db := (num+1, update_db false consts db);
      thm
   end;