src/ZF/Perm.ML

--- a/src/ZF/Perm.ML	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Perm.ML	Mon Dec 28 16:59:28 1998 +0100
@@ -71,7 +71,7 @@
 
 Goal "[| f: A->B;  ALL x:A. d(f`x)=x |] ==> f: inj(A,B)";
 by (asm_simp_tac (simpset() addsimps [inj_def]) 1);
-by (deepen_tac (claset() addEs [subst_context RS box_equals]) 0 1);
+by (blast_tac (claset() addIs [subst_context RS box_equals]) 1);
 bind_thm ("f_imp_injective", ballI RSN (2,result()));
 
 val prems = Goal