src/LCF/LCF.thy

--- a/src/LCF/LCF.thy	Thu Jun 01 23:07:51 2006 +0200
+++ b/src/LCF/LCF.thy	Thu Jun 01 23:09:34 2006 +0200
@@ -370,7 +370,8 @@
   shows "P(FIX(f),FIX(g))"
   apply (rule FIX1 [THEN ssubst, of _ f g])
   apply (rule FIX2 [THEN ssubst, of _ f g])
-  apply (rule induct [OF 1, where ?f = "%x. <f(FST(x)),g(SND(x))>"])
+  apply (rule induct [where ?f = "%x. <f(FST(x)),g(SND(x))>"])
+  apply (rule 1)
   apply simp
   apply (rule 2)
   apply (simp add: expand_all_PROD)