
diff -r 886655a150f6 -r d1b97708d5eb src/CCL/Fix.thy
--- a/src/CCL/Fix.thy	Thu Jun 21 20:48:48 2007 +0200
+++ b/src/CCL/Fix.thy	Thu Jun 21 22:10:16 2007 +0200
@@ -181,9 +181,10 @@
   done
 
 lemma term_ind:
-  assumes "P(bot)" "P(true)" "P(false)"
-    "!!x y.[| P(x);  P(y) |] ==> P(<x,y>)"
-    "!!u.(!!x. P(u(x))) ==> P(lam x. u(x))"  "INCL(P)"
+  assumes 1: "P(bot)" and 2: "P(true)" and 3: "P(false)"
+    and 4: "!!x y.[| P(x);  P(y) |] ==> P(<x,y>)"
+    and 5: "!!u.(!!x. P(u(x))) ==> P(lam x. u(x))"
+    and 6: "INCL(P)"
   shows "P(t)"
   apply (rule reachability [THEN id_apply, THEN subst])
   apply (rule_tac x = t in spec)
@@ -191,12 +192,12 @@
     apply (unfold idgen_def)
     apply (rule allI)
     apply (subst applyBbot)
-    apply assumption
+    apply (rule 1)
    apply (rule allI)
    apply (rule applyB [THEN ssubst])
     apply (rule_tac t = "xa" in term_case)
        apply simp_all
-       apply (fast intro: prems INCL_subst all_INCL)+
+       apply (fast intro: assms INCL_subst all_INCL)+
   done
 
 end




