src/ZF/AC/WO6_WO1.thy

--- a/src/ZF/AC/WO6_WO1.thy	Tue Feb 14 20:57:05 2012 +0100
+++ b/src/ZF/AC/WO6_WO1.thy	Tue Feb 14 21:19:39 2012 +0100
@@ -526,7 +526,7 @@
 apply (rule allI)
 apply (case_tac "A=0")
 apply (fast intro!: well_ord_Memrel nat_0I [THEN nat_into_Ord])
-apply (rule_tac x1 = A in lemma_iv [THEN revcut_rl])
+apply (rule_tac x = A in lemma_iv [elim_format])
 apply (erule exE)
 apply (drule WO6_imp_NN_not_empty)
 apply (erule Un_subset_iff [THEN iffD1, THEN conjE])