--- a/src/HOL/Fun.ML Fri Aug 14 12:02:35 1998 +0200
+++ b/src/HOL/Fun.ML Fri Aug 14 12:03:01 1998 +0200
@@ -78,7 +78,7 @@
by (rtac iffI 1);
by (etac arg_cong 2);
by (etac injD 1);
-ba 1;
+by (assume_tac 1);
qed "inj_eq";
Goal "inj(f) ==> (@x. f(x)=f(y)) = y";