src/ZF/Perm.ML

--- a/src/ZF/Perm.ML	Thu May 15 15:51:09 1997 +0200
+++ b/src/ZF/Perm.ML	Thu May 15 15:51:47 1997 +0200
@@ -540,7 +540,7 @@
     "!!f. [| f: inj(A,B);  a~:A;  b~:B |]  ==> \
 \         cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
 by (fast_tac (!claset addIs [apply_type]
-               unsafe_addss (!simpset addsimps [fun_extend, fun_extend_apply2,
+               addss (!simpset addsimps [fun_extend, fun_extend_apply2,
 						fun_extend_apply1])) 1);
 qed "inj_extend";