# HG changeset patch
# User paulson
# Date 910960066 -3600
# Node ID 1f72c4233a8b87fc8ed2f302f58665ff28b48df4
# Parent  36b5559d822494be5cc86cb7529a466b3fe55d4c
moved UNION_o to Fun.ML, since Fun.thy is no longer a parent of equalities

diff -r 36b5559d8224 -r 1f72c4233a8b src/HOL/equalities.ML
--- 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...*)