# HG changeset patch
# User wenzelm
# Date 911472299 -3600
# Node ID 7b0f502a25b12b491f08f24070f3c68eccf45c9d
# Parent  737559a43e7190d1ad2dcda9839a9b8fc10ac1fd
no warning for "it" theorems;

diff -r 737559a43e71 -r 7b0f502a25b1 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Nov 18 16:24:33 1998 +0100
+++ b/src/Pure/pure_thy.ML	Thu Nov 19 11:44:59 1998 +0100
@@ -204,7 +204,8 @@
 
 (* naming *)
 
-val default_name = fn "" => "it" | name => name;
+val defaultN = "it";
+val default_name = fn "" => defaultN | name => name;
 
 fun gen_names len name =
   map (fn i => name ^ "_" ^ string_of_int i) (1 upto len);
@@ -215,11 +216,13 @@
 
 (* enter_tthmx *)
 
+fun cond_warning name msg = if Sign.base_name name = defaultN then () else warning msg;
+
 fun warn_overwrite name =
-  warning ("Replaced old copy of theorems " ^ quote name);
+  cond_warning name ("Replaced old copy of theorems " ^ quote name);
 
 fun warn_same name =
-  warning ("Theorem database already contains a copy of " ^ quote name);
+  cond_warning name ("Theorem database already contains a copy of " ^ quote name);
 
 fun enter_tthmx sg app_name (bname, tthmx) =
   let