src/HOL/Probability/Radon_Nikodym.thy

--- a/src/HOL/Probability/Radon_Nikodym.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -1295,7 +1295,7 @@
   have "density M (RN_deriv M N) {x} = (\<integral>\<^sup>+w. RN_deriv M N x * indicator {x} w \<partial>M)"
     by (auto simp: indicator_def emeasure_density intro!: nn_integral_cong)
   with x density_RN_deriv[OF ac] RN_deriv_nonneg[of M N] show ?thesis
-    by (auto simp: nn_integral_cmult_indicator)
+    by (auto simp: max_def)
 qed
 
 end