--- a/src/CCL/Type.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/CCL/Type.thy Wed Mar 19 22:50:42 2008 +0100
@@ -397,7 +397,7 @@
val lfpI = thm "lfpI"
val coinduct3_mono_lemma = thm "coinduct3_mono_lemma"
fun mk_thm s = prove_goal (the_context ()) s (fn mono::prems =>
- [fast_tac (claset () addIs ((mono RS coinduct3_mono_lemma RS lfpI)::prems)) 1])
+ [fast_tac (@{claset} addIs ((mono RS coinduct3_mono_lemma RS lfpI)::prems)) 1])
in
val ci3_RI = mk_thm "[| mono(Agen); a : R |] ==> a : lfp(%x. Agen(x) Un R Un A)"
val ci3_AgenI = mk_thm "[| mono(Agen); a : Agen(lfp(%x. Agen(x) Un R Un A)) |] ==> a : lfp(%x. Agen(x) Un R Un A)"
@@ -405,8 +405,8 @@
fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s
(fn prems => [rtac (genXH RS iffD2) 1,
- simp_tac (simpset ()) 1,
- TRY (fast_tac (claset () addIs
+ SIMPSET' simp_tac 1,
+ TRY (fast_tac (@{claset} addIs
([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI]
@ prems)) 1)])
end;