src/ZF/AC/AC16_WO4.ML

 \       ==> (lam a:succ(A). if(a=A, y, f`a)) : inj(succ(A), B)";
 by (res_inst_tac [("d","%z. if(z=y, A, converse(f)`z)")] lam_injective 1);
 by (ALLGOALS
     (asm_simp_tac 
      (simpset() addsimps [inj_is_fun RS apply_type, left_inverse] 
-      setloop (split_tac [expand_if] ORELSE' Step_tac))));
+      setloop (split_tac [split_if] ORELSE' Step_tac))));
 qed "succ_not_lepoll_lemma";
 
 Goalw [lepoll_def, eqpoll_def, bij_def, surj_def]
         "!!A. [| ~A eqpoll B; A lepoll B |] ==> succ(A) lepoll B";
 by (fast_tac (claset() addSEs [succ_not_lepoll_lemma, inj_is_fun]) 1);