--- a/src/HOL/Analysis/Caratheodory.thy Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Caratheodory.thy Mon Jan 14 18:35:03 2019 +0000
@@ -664,7 +664,7 @@
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