diff -r c061e6f9d546 -r c9ad6bbf3a34 src/ZF/AC/Cardinal_aux.ML
--- a/src/ZF/AC/Cardinal_aux.ML	Thu Aug 13 18:07:38 1998 +0200
+++ b/src/ZF/AC/Cardinal_aux.ML	Thu Aug 13 18:07:56 1998 +0200
@@ -57,8 +57,7 @@
 qed "Un_eqpoll_Inf_Ord";
 
 
-(*bijection is inferred!*)
-Goal "(lam u:{{y,z} . y: x}. THE y. {y,z} = u) : bij({{y,z}. y:x}, x)";
+Goal "?f : bij({{y,z}. y:x}, x)";
 by (rtac RepFun_bijective 1);
 by (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1);
 by (Blast_tac 1);