src/ZF/AC/WO1_WO7.thy

--- a/src/ZF/AC/WO1_WO7.thy	Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/WO1_WO7.thy	Mon Jan 21 11:25:45 2002 +0100
@@ -50,7 +50,7 @@
 lemma converse_Memrel_not_wf_on: 
     "[| Ord(a); ~Finite(a) |] ==> ~wf[a](converse(Memrel(a)))"
 apply (unfold wf_on_def wf_def)
-apply (drule nat_le_infinite_Ord [THEN le_imp_subset], (assumption))
+apply (drule nat_le_infinite_Ord [THEN le_imp_subset], assumption)
 apply (rule notI)
 apply (erule_tac x = "nat" in allE, blast)
 done