diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Binary_Product_Measure.thy
--- a/src/HOL/Analysis/Binary_Product_Measure.thy	Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Sun Nov 18 18:07:51 2018 +0000
@@ -1118,7 +1118,7 @@
         unfolding * by auto
     next
       case (Union A)
-      moreover have *: "(UNION UNIV A) \<times> UNIV = UNION UNIV (\<lambda>i. A i \<times> UNIV)"
+      moreover have *: "(\<Union>(A ` UNIV)) \<times> UNIV = \<Union>((\<lambda>i. A i \<times> UNIV) ` UNIV)"
         by auto
       ultimately show ?case
         unfolding * by auto
@@ -1137,7 +1137,7 @@
         unfolding * by auto
     next
       case (Union B)
-      moreover have *: "UNIV \<times> (UNION UNIV B) = UNION UNIV (\<lambda>i. UNIV \<times> B i)"
+      moreover have *: "UNIV \<times> (\<Union>(B ` UNIV)) = \<Union>((\<lambda>i. UNIV \<times> B i) ` UNIV)"
         by auto
       ultimately show ?case
         unfolding * by auto