--- a/src/HOL/Probability/Bochner_Integration.thy Sun Dec 27 17:16:21 2015 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy Sun Dec 27 21:46:36 2015 +0100
@@ -2494,7 +2494,7 @@
from nonneg have "AE x in M. mono (\<lambda>n::nat. f x * indicator {..real n} x)"
by (auto split: split_indicator intro!: monoI)
{ fix x have "eventually (\<lambda>n. f x * indicator {..real n} x = f x) sequentially"
- by (rule eventually_sequentiallyI[of "nat(ceiling x)"])
+ by (rule eventually_sequentiallyI[of "nat \<lceil>x\<rceil>"])
(auto split: split_indicator simp: nat_le_iff ceiling_le_iff) }
from filterlim_cong[OF refl refl this]
have "AE x in M. (\<lambda>i. f x * indicator {..real i} x) ----> f x"