--- a/src/HOL/Analysis/Caratheodory.thy Sun Dec 30 10:34:56 2018 +0000
+++ b/src/HOL/Analysis/Caratheodory.thy Sun Dec 30 10:34:56 2018 +0000
@@ -737,7 +737,7 @@
using f C Ai unfolding bij_betw_def by auto
then have "\<Union>range f = A i"
using f C Ai unfolding bij_betw_def
- by (auto simp add: f_def cong del: SUP_cong_strong)
+ by (auto simp add: f_def cong del: SUP_cong_simp)
moreover
{ have "(\<Sum>j. \<mu>_r (f j)) = (\<Sum>j. if j \<in> {..< card C} then \<mu>_r (f j) else 0)"
using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def)