src/ZF/Perm.ML

--- a/src/ZF/Perm.ML	Mon Sep 21 23:16:25 1998 +0200
+++ b/src/ZF/Perm.ML	Mon Sep 21 23:17:28 1998 +0200
@@ -544,8 +544,8 @@
 Goalw [inj_def]
     "[| 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]
-               addss (simpset() addsimps [fun_extend, fun_extend_apply2,
-						fun_extend_apply1])) 1);
+by (force_tac (claset() addIs [apply_type],
+               simpset() addsimps [fun_extend, fun_extend_apply2,
+						fun_extend_apply1]) 1);
 qed "inj_extend";