diff -r 123401a5c8e9 -r 5e309df58557 CookBook/Package/Ind_Examples.thy
--- a/CookBook/Package/Ind_Examples.thy	Fri Feb 06 06:19:52 2009 +0000
+++ b/CookBook/Package/Ind_Examples.thy	Sat Feb 07 12:05:02 2009 +0000
@@ -128,12 +128,15 @@
   apply (unfold trcl_def)
   apply (rule allI impI)+
   proof -
-    case goal1
+    case (goal1 P)
+    have g1: "R x y" by fact
+    have g2: "\<forall>P. (\<forall>x. P x x) \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P y z" by fact
+    have g3: "\<forall>x. P x x" by fact
+    have g4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact
     show ?case
-      apply (rule goal1(4) [rule_format])
-      apply (rule goal1(1))
-      apply (rule goal1(2) [THEN spec [where x=P], THEN mp, THEN mp,
-	OF goal1(3-4)])
+      apply (rule g4 [rule_format])
+      apply (rule g1)
+      apply (rule g2 [THEN spec [where x=P], THEN mp, THEN mp, OF g3, OF g4])
       done
   qed