--- a/src/HOL/equalities.ML Mon Feb 28 13:39:45 2000 +0100
+++ b/src/HOL/equalities.ML Tue Feb 29 10:41:08 2000 +0100
@@ -558,13 +558,13 @@
qed "Inter_image_eq";
Addsimps [Inter_image_eq];
-Goal "u: A ==> (UN y:A. c) = c";
-by (Blast_tac 1);
+Goal "(UN y:A. c) = (if A={} then {} else c)";
+by Auto_tac;
qed "UN_constant";
Addsimps[UN_constant];
-Goal "u: A ==> (INT y:A. c) = c";
-by (Blast_tac 1);
+Goal "(INT y:A. c) = (if A={} then UNIV else c)";
+by Auto_tac;
qed "INT_constant";
Addsimps[INT_constant];