diff -r 9f35f2744fa8 -r 2e9a86203d59 equalities.ML
--- a/equalities.ML	Thu Mar 17 11:27:29 1994 +0100
+++ b/equalities.ML	Thu Mar 17 14:08:08 1994 +0100
@@ -186,7 +186,7 @@
 
 goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
 by (fast_tac eq_cs 1);
-val Int_Union_image = result();
+val Int_Union = result();
 
 (* Devlin, page 12: Union of a family of unions **)
 goal Set.thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
@@ -195,7 +195,7 @@
 
 goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
 by (fast_tac eq_cs 1);
-val Un_Inter_image = result();
+val Un_Inter = result();
 
 goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
 by (best_tac eq_cs 1);