# HG changeset patch
# User paulson
# Date 949331991 -3600
# Node ID db112d36a426374b6d8736fa83b7ca5dd20252c9
# Parent  7d08b047b76e300bd159e5796f43f808a151de1d
renamed image_Union_eq -> image_Union

diff -r 7d08b047b76e -r db112d36a426 src/HOL/equalities.ML
--- 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);