src/HOL/Analysis/Radon_Nikodym.thy

     show "countable (range (\<lambda>(i, j). A i \<inter> Q j))"
       by auto
     show "range (\<lambda>(i, j). A i \<inter> Q j) \<subseteq> sets (density M f)"
       using A_in_sets by auto
   next
-    have "\<Union>range (\<lambda>(i, j). A i \<inter> Q j) = (\<Union>i j. A i \<inter> Q j)"
+    have "\<Union>(range (\<lambda>(i, j). A i \<inter> Q j)) = (\<Union>i j. A i \<inter> Q j)"
       by auto
     also have "\<dots> = (\<Union>i. A i) \<inter> space M" using Q by auto
     also have "(\<Union>i. A i) = space M"
     proof safe
       fix x assume x: "x \<in> space M"

           by simp
         finally show ?thesis
           using x real by (auto simp: A_def ennreal_of_nat_eq_real_of_nat intro!: exI[of _ "Suc n"])
       qed
     qed (auto simp: A_def)
-    finally show "\<Union>range (\<lambda>(i, j). A i \<inter> Q j) = space ?N" by simp
+    finally show "\<Union>(range (\<lambda>(i, j). A i \<inter> Q j)) = space ?N" by simp
   next
     fix X assume "X \<in> range (\<lambda>(i, j). A i \<inter> Q j)"
     then obtain i j where [simp]:"X = A i \<inter> Q j" by auto
     have "(\<integral>\<^sup>+x. f x * indicator (A i \<inter> Q j) x \<partial>M) \<noteq> \<infinity>"
     proof (cases i)