diff -r 2f5a4367a39e -r 0f65fa163304 src/CCL/Type.thy
--- 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;