# HG changeset patch
# User paulson
# Date 929608413 -7200
# Node ID f8aed3706af76bf12666ca4d7f1f28970cb654a9
# Parent  50459a995aa35125fd4bbf64db2f083112c7f6b4
renamed UNION_... to UN_... (to fit the convention)

diff -r 50459a995aa3 -r f8aed3706af7 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Thu Jun 17 10:32:52 1999 +0200
+++ b/src/HOL/Prod.ML	Thu Jun 17 10:33:33 1999 +0200
@@ -379,7 +379,7 @@
 (*Suggested by Pierre Chartier*)
 Goal "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
 by (Blast_tac 1);
-qed "UNION_Times_distrib";
+qed "UN_Times_distrib";
 
 Goal "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))";
 by (Fast_tac 1);