src/CCL/Type.thy

--- a/src/CCL/Type.thy	Tue Apr 26 21:55:11 2011 +0200
+++ b/src/CCL/Type.thy	Tue Apr 26 22:18:07 2011 +0200
@@ -417,10 +417,10 @@
 
 ML {*
 fun genIs_tac ctxt genXH gen_mono =
-  rtac (genXH RS iffD2) THEN'
+  rtac (genXH RS @{thm iffD2}) THEN'
   simp_tac (simpset_of ctxt) THEN'
   TRY o fast_tac (claset_of ctxt addIs
-        [genXH RS iffD2, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}])
+        [genXH RS @{thm iffD2}, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}])
 *}
 
 method_setup genIs = {*