src/ZF/AC/WO2_AC16.thy

--- a/src/ZF/AC/WO2_AC16.thy	Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/AC/WO2_AC16.thy	Sun Nov 20 20:15:02 2011 +0100
@@ -315,8 +315,7 @@
 
 lemmas disj_Un_eqpoll_nat_sum = 
     eqpoll_trans [THEN eqpoll_trans, 
-                  OF disj_Un_eqpoll_sum sum_eqpoll_cong nat_sum_eqpoll_sum,
-                  standard];
+                  OF disj_Un_eqpoll_sum sum_eqpoll_cong nat_sum_eqpoll_sum];
 
 
 lemma Un_in_Collect: "[| x \<in> Pow(A - B - h`i); x\<approx>m;