# HG changeset patch
# User wenzelm
# Date 1180614847 -7200
# Node ID 6ec9e29143e94c641b29ab4f1b7206cbf48044a2
# Parent  4b04f9d859afdb5c3940951bac397907beba1ed9
removed obsolete IFOL.thy/FOL.thy values;

diff -r 4b04f9d859af -r 6ec9e29143e9 src/FOL/ex/ROOT.ML
--- a/src/FOL/ex/ROOT.ML	Thu May 31 14:34:06 2007 +0200
+++ b/src/FOL/ex/ROOT.ML	Thu May 31 14:34:07 2007 +0200
@@ -15,7 +15,7 @@
 
 time_use_thy "Intuitionistic";
 
-val thy = IFOL.thy  and  tac = IntPr.fast_tac 1;
+val thy = theory "IFOL"  and  tac = IntPr.fast_tac 1;
 time_use     "prop.ML";
 time_use     "quant.ML";
 
@@ -24,7 +24,7 @@
 time_use_thy "Classical";
 time_use_thy "If";
 
-val thy = FOL.thy  and  tac = Cla.fast_tac FOL_cs 1;
+val thy = theory "FOL"  and  tac = Cla.fast_tac FOL_cs 1;
 time_use     "prop.ML";
 time_use     "quant.ML";
 
diff -r 4b04f9d859af -r 6ec9e29143e9 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Thu May 31 14:34:06 2007 +0200
+++ b/src/ZF/ind_syntax.ML	Thu May 31 14:34:07 2007 +0200
@@ -125,7 +125,7 @@
     let val rec_hds = map head_of rec_tms
         val dummy = assert_all is_Const rec_hds
           (fn t => "Datatype set not previously declared as constant: " ^
-                   Sign.string_of_term IFOL.thy t);
+                   Sign.string_of_term @{theory IFOL} t);
         val rec_names = (*nat doesn't have to be added*)
 	    "Nat.nat" :: map (#1 o dest_Const) rec_hds
 	val u = if co then quniv else univ