diff -r e0f68a507683 -r b021008c5397 src/HOL/Probability/Tree_Space.thy
--- a/src/HOL/Probability/Tree_Space.thy	Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Probability/Tree_Space.thy	Sun Nov 18 18:07:51 2018 +0000
@@ -197,7 +197,7 @@
     finally show ?case .
   next
     case (Union I)
-    have *: "{Node l v r |l v r. (v, l, r) \<in> UNION UNIV I} =
+    have *: "{Node l v r |l v r. (v, l, r) \<in> \<Union>(I ` UNIV)} =
       (\<Union>i. {Node l v r |l v r. (v, l, r) \<in> I i})" by auto
     show ?case unfolding * using Union(2) by (intro sets.countable_UN) auto
   qed