removed obsolete IFOL.thy/FOL.thy values;
authorwenzelm
Thu May 31 14:34:07 2007 +0200 (2007-05-31 ago)
changeset 231566ec9e29143e9
parent 23155 4b04f9d859af
child 23157 340586b2305c
removed obsolete IFOL.thy/FOL.thy values;
src/FOL/ex/ROOT.ML
src/ZF/ind_syntax.ML
     1.1 --- a/src/FOL/ex/ROOT.ML	Thu May 31 14:34:06 2007 +0200
     1.2 +++ b/src/FOL/ex/ROOT.ML	Thu May 31 14:34:07 2007 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  time_use_thy "Intuitionistic";
     1.6  
     1.7 -val thy = IFOL.thy  and  tac = IntPr.fast_tac 1;
     1.8 +val thy = theory "IFOL"  and  tac = IntPr.fast_tac 1;
     1.9  time_use     "prop.ML";
    1.10  time_use     "quant.ML";
    1.11  
    1.12 @@ -24,7 +24,7 @@
    1.13  time_use_thy "Classical";
    1.14  time_use_thy "If";
    1.15  
    1.16 -val thy = FOL.thy  and  tac = Cla.fast_tac FOL_cs 1;
    1.17 +val thy = theory "FOL"  and  tac = Cla.fast_tac FOL_cs 1;
    1.18  time_use     "prop.ML";
    1.19  time_use     "quant.ML";
    1.20  
     2.1 --- a/src/ZF/ind_syntax.ML	Thu May 31 14:34:06 2007 +0200
     2.2 +++ b/src/ZF/ind_syntax.ML	Thu May 31 14:34:07 2007 +0200
     2.3 @@ -125,7 +125,7 @@
     2.4      let val rec_hds = map head_of rec_tms
     2.5          val dummy = assert_all is_Const rec_hds
     2.6            (fn t => "Datatype set not previously declared as constant: " ^
     2.7 -                   Sign.string_of_term IFOL.thy t);
     2.8 +                   Sign.string_of_term @{theory IFOL} t);
     2.9          val rec_names = (*nat doesn't have to be added*)
    2.10  	    "Nat.nat" :: map (#1 o dest_Const) rec_hds
    2.11  	val u = if co then quniv else univ