diff -r b58a575d211e -r 62e47f06d22c src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Tue Mar 05 07:00:21 2019 +0000
@@ -880,7 +880,7 @@
   also have "\<dots> = (\<integral>\<^sup>+ x. (SUP i. F i x) \<partial>join M)"
     using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq)
                  (simp_all add: M cong: measurable_cong_sets)
-  finally show ?case by (simp add: ac_simps)
+  finally show ?case by (simp add: ac_simps image_comp)
 qed
 
 lemma measurable_join1: