replaced UN_constant, INT_constant by unconditional versions that rewrite
to if-then-else expressions

--- 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];