diff -r 3294f727e20d -r b9f6154427a4 src/ZF/Zorn.thy
--- a/src/ZF/Zorn.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Zorn.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -115,7 +115,7 @@
 apply (erule TFin_induct)
 apply (rule impI [THEN ballI])
 txt{*case split using @{text TFin_linear_lemma1}*}
-apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
+apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
        assumption+)
 apply (blast del: subsetI
 	     intro: increasing_trans subsetI, blast)
@@ -127,7 +127,7 @@
 apply (rule ballI)
 apply (drule bspec, assumption)
 apply (drule subsetD, assumption)
-apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
+apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
        assumption+, blast)
 apply (erule increasingD2 [THEN subset_trans, THEN disjI1])
 apply (blast dest: TFin_is_subset)+
@@ -156,8 +156,7 @@
      "[| n \<in> TFin(S,next);  m \<in> TFin(S,next);  m = next`m |] ==> n <= m"
 apply (erule TFin_induct)
 apply (drule TFin_subsetD)
-apply (assumption+, force)
-apply blast
+apply (assumption+, force, blast)
 done
 
 text{*Property 3.3 of section 3.3*}
@@ -208,8 +207,7 @@
      "[| ch \<in> (\<Pi>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
       ==> ch ` super(S,X) \<noteq> X"
 apply (rule notI)
-apply (drule choice_super, assumption)
-apply assumption
+apply (drule choice_super, assumption, assumption)
 apply (simp add: super_def)
 done