no warning for "it" theorems;

--- 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