diff -r 804c8a178a7f -r c068bd2f0bbd src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Thu Jun 05 14:40:35 1997 +0200
+++ b/src/HOL/Finite.ML	Thu Jun 05 17:19:05 1997 +0200
@@ -128,12 +128,6 @@
 qed "finite_Diff_singleton";
 AddIffs [finite_Diff_singleton];
 
-(*** FIXME -> equalities.ML ***)
-goal Set.thy "(f``A = {}) = (A = {})";
-by (blast_tac (!claset addSEs [equalityE]) 1);
-qed "image_is_empty";
-Addsimps [image_is_empty];
-
 goal Finite.thy "!!A. finite B ==> !A. f``A = B --> inj_onto f A --> finite A";
 by (etac finite_induct 1);
  by (ALLGOALS Asm_simp_tac);