diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Thu May 26 17:51:22 2016 +0200
@@ -1648,7 +1648,7 @@
       using sums_If_finite[of "\<lambda>r. r < f x" "\<lambda>_. 1 :: ennreal"]
       by (cases "f x") (simp_all add: sums_def of_nat_tendsto_top_ennreal)
     also have "(\<lambda>i. (if i < f x then 1 else 0)) = (\<lambda>i. indicator (F i) x)"
-      using `x \<in> space M` by (simp add: one_ennreal_def F_def fun_eq_iff)
+      using \<open>x \<in> space M\<close> by (simp add: one_ennreal_def F_def fun_eq_iff)
     finally have "ennreal_of_enat (f x) = (\<Sum>i. indicator (F i) x)"
       by (simp add: sums_iff) }
   then have "(\<integral>\<^sup>+x. ennreal_of_enat (f x) \<partial>M) = (\<integral>\<^sup>+x. (\<Sum>i. indicator (F i) x) \<partial>M)"