diff -r 349c639e593c -r 7643b005b29a src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Probability/Information.thy	Sun Apr 15 13:57:00 2018 +0100
@@ -834,9 +834,14 @@
     - log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX)"
     using Px Px_nn fin by (auto simp: measure_def)
   also have "- log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX) = - log b (\<integral> x. 1 / Px x \<partial>distr M MX X)"
-    unfolding distributed_distr_eq_density[OF X] using Px Px_nn
-    apply (intro arg_cong[where f="log b"] arg_cong[where f=uminus])
-    by (subst integral_density) (auto simp del: integral_indicator intro!: Bochner_Integration.integral_cong)
+  proof -
+    have "integral\<^sup>L MX (indicator {x \<in> space MX. Px x \<noteq> 0}) = LINT x|MX. Px x *\<^sub>R (1 / Px x)"
+      by (rule Bochner_Integration.integral_cong) auto
+    also have "... = LINT x|density MX (\<lambda>x. ennreal (Px x)). 1 / Px x"
+      by (rule integral_density [symmetric]) (use Px Px_nn in auto)
+    finally show ?thesis
+      unfolding distributed_distr_eq_density[OF X] by simp
+  qed
   also have "\<dots> \<le> (\<integral> x. - log b (1 / Px x) \<partial>distr M MX X)"
   proof (rule X.jensens_inequality[of "\<lambda>x. 1 / Px x" "{0<..}" 0 1 "\<lambda>x. - log b x"])
     show "AE x in distr M MX X. 1 / Px x \<in> {0<..}"