diff -r 8460ddd478d2 -r 707b6f9859d2 src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Wed Feb 03 15:49:24 1999 +0100
+++ b/src/ZF/Cardinal.ML	Wed Feb 03 15:50:37 1999 +0100
@@ -562,7 +562,7 @@
     lam_injective 1);
 by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_type, cons_iff]
                         setloop etac consE') 1);
-by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_type, left_inverse]
+by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_type]
                         setloop etac consE') 1);
 qed "cons_lepoll_cong";
 
@@ -616,10 +616,9 @@
 by (blast_tac (claset() addSIs [if_type, inj_is_fun RS apply_type]) 1);
 by (asm_simp_tac 
     (simpset() addsimps [inj_converse_fun RS apply_funtype]) 1);
-by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_rangeI, left_inverse]
+by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_rangeI]
                         setloop etac UnE') 1);
-by (asm_simp_tac 
-    (simpset() addsimps [inj_converse_fun RS apply_funtype, right_inverse]) 1);
+by (asm_simp_tac (simpset() addsimps [inj_converse_fun RS apply_funtype]) 1);
 by (Blast_tac 1);
 qed "inj_disjoint_eqpoll";