diff -r 9bbd5497befd -r 3d954183b707 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Sat Nov 10 07:57:19 2018 +0000
+++ b/src/HOL/Lattices_Big.thy	Sat Nov 10 07:57:20 2018 +0000
@@ -370,7 +370,7 @@
     by (rule finite_surj [where f = "sup x", OF B(1)], auto)
   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
   proof -
-    have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
+    have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (\<Union>a\<in>A. \<Union>b\<in>B. {sup a b})"
       by blast
     thus ?thesis by(simp add: insert(1) B(1))
   qed
@@ -407,7 +407,7 @@
     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
   proof -
-    have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
+    have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (\<Union>a\<in>A. \<Union>b\<in>B. {inf a b})"
       by blast
     thus ?thesis by(simp add: insert(1) B(1))
   qed