--- a/src/HOL/equalities.ML Mon Jan 31 16:19:14 2000 +0100
+++ b/src/HOL/equalities.ML Mon Jan 31 16:19:51 2000 +0100
@@ -551,7 +551,7 @@
Goal "f `` Union S = (UN x:S. f `` x)";
by (Blast_tac 1);
-qed "image_Union_eq";
+qed "image_Union";
Goal "Inter(B``A) = (INT x:A. B(x))";
by (Blast_tac 1);