no warning for "it" theorems;
authorwenzelm
Thu Nov 19 11:44:59 1998 +0100 (1998-11-19)
changeset 59337b0f502a25b1
parent 5932 737559a43e71
child 5934 ecc224b81f7f
no warning for "it" theorems;
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/pure_thy.ML	Wed Nov 18 16:24:33 1998 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Thu Nov 19 11:44:59 1998 +0100
     1.3 @@ -204,7 +204,8 @@
     1.4  
     1.5  (* naming *)
     1.6  
     1.7 -val default_name = fn "" => "it" | name => name;
     1.8 +val defaultN = "it";
     1.9 +val default_name = fn "" => defaultN | name => name;
    1.10  
    1.11  fun gen_names len name =
    1.12    map (fn i => name ^ "_" ^ string_of_int i) (1 upto len);
    1.13 @@ -215,11 +216,13 @@
    1.14  
    1.15  (* enter_tthmx *)
    1.16  
    1.17 +fun cond_warning name msg = if Sign.base_name name = defaultN then () else warning msg;
    1.18 +
    1.19  fun warn_overwrite name =
    1.20 -  warning ("Replaced old copy of theorems " ^ quote name);
    1.21 +  cond_warning name ("Replaced old copy of theorems " ^ quote name);
    1.22  
    1.23  fun warn_same name =
    1.24 -  warning ("Theorem database already contains a copy of " ^ quote name);
    1.25 +  cond_warning name ("Theorem database already contains a copy of " ^ quote name);
    1.26  
    1.27  fun enter_tthmx sg app_name (bname, tthmx) =
    1.28    let