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