# HG changeset patch
# User wenzelm
# Date 1149196174 -7200
# Node ID 093690d4ba606c57a2ae52333748791892593f66
# Parent  4a2a71c3196865ffa3f3516ef0ee1edc63043a4f
tuned;

diff -r 4a2a71c31968 -r 093690d4ba60 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)