diff -r d5178f19b671 -r 2a858377c3d2 src/ZF/AC/HH.thy
--- a/src/ZF/AC/HH.thy	Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/AC/HH.thy	Sun Nov 20 20:15:02 2011 +0100
@@ -210,7 +210,7 @@
   simplification is needed!*)
 lemmas bij_Least_HH_x =  
     comp_bij [OF f_sing_lam_bij [OF _ lam_singI] 
-              lam_sing_bij [THEN bij_converse_bij], standard]
+              lam_sing_bij [THEN bij_converse_bij]]
 
 
 subsection{*The proof of AC1 ==> WO2*}