diff -r 6288ebcb1623 -r 75ca1bf5ae12 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Wed Feb 13 10:45:08 2002 +0100
+++ b/src/HOL/Fun.ML	Wed Feb 13 10:48:29 2002 +0100
@@ -283,7 +283,7 @@
 qed "inj_image_subset_iff";
 
 Goal "inj f ==> (f`A = f`B) = (A = B)";
-by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1);
+by (blast_tac (claset() addDs [injD]) 1);
 qed "inj_image_eq_iff";
 
 Goal  "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))";