--- a/src/HOL/equalities.ML Fri Nov 13 13:27:03 1998 +0100
+++ b/src/HOL/equalities.ML Fri Nov 13 13:27:46 1998 +0100
@@ -521,10 +521,6 @@
by (Blast_tac 1);
qed "INT_eq";
-Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
-by (Blast_tac 1);
-qed "UNION_o";
-
(*Distributive laws...*)