src/HOL/Analysis/Caratheodory.thy

     note F'_disj = this
     define F where "F i = (if i < card C then F' i else {})" for i
     then have "disjoint_family F"
       using F'_disj by (auto simp: disjoint_family_on_def)
     moreover from F' have "(\<Union>i. F i) = \<Union>C"
-      by (auto simp add: F_def split: if_split_asm) blast
+      by (auto simp add: F_def split: if_split_asm cong del: SUP_cong)
     moreover have sets_F: "\<And>i. F i \<in> M"
       using F' sets_C by (auto simp: F_def)
     moreover note sets_C
     ultimately have "\<mu> (\<Union>C) = (\<Sum>i. \<mu> (F i))"
       using ca[unfolded countably_additive_def, THEN spec, of F] by auto