diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Probability/Levy.thy
--- a/src/HOL/Probability/Levy.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/Levy.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -136,9 +136,9 @@
     have "(CLBINT t=-T..T. ?F t * \<phi> t) =
       (CLBINT t. (CLINT x | M. ?F t * iexp (t * x) * indicator {-T<..<T} t))"
       using \<open>T \<ge> 0\<close> unfolding \<phi>_def char_def interval_lebesgue_integral_def
-      by (auto split: split_indicator intro!: integral_cong)
+      by (auto split: split_indicator intro!: Bochner_Integration.integral_cong)
     also have "\<dots> = (CLBINT t. (CLINT x | M. ?f' (t, x)))"
-      by (auto intro!: integral_cong simp: field_simps exp_diff exp_minus split: split_indicator)
+      by (auto intro!: Bochner_Integration.integral_cong simp: field_simps exp_diff exp_minus split: split_indicator)
     also have "\<dots> = (CLINT x | M. (CLBINT t. ?f' (t, x)))"
     proof (intro P.Fubini_integral [symmetric] integrableI_bounded_set [where B="b - a"])
       show "emeasure (lborel \<Otimes>\<^sub>M M) ({- T<..<T} \<times> space M) < \<infinity>"
@@ -151,7 +151,7 @@
     qed (auto split: split_indicator split_indicator_asm)
     also have "\<dots> = (CLINT x | M. (complex_of_real (2 * (sgn (x - a) *
          Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))))"
-       using main_eq by (intro integral_cong, auto)
+       using main_eq by (intro Bochner_Integration.integral_cong, auto)
     also have "\<dots> = complex_of_real (LINT x | M. (2 * (sgn (x - a) *
          Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b)))))"
        by (rule integral_complex_of_real)
@@ -336,11 +336,11 @@
         (CLBINT t:{-u..u}. (CLINT x | M n. 1 - iexp (t * x)))"
       unfolding char_def by (rule set_lebesgue_integral_cong, auto simp del: of_real_mult)
     also have "\<dots> = (CLBINT t. (CLINT x | M n. indicator {-u..u} t *\<^sub>R (1 - iexp (t * x))))"
-      by (rule integral_cong) (auto split: split_indicator)
+      by (rule Bochner_Integration.integral_cong) (auto split: split_indicator)
     also have "\<dots> = (CLINT x | M n. (CLBINT t:{-u..u}. 1 - iexp (t * x)))"
       using Mn3 by (subst P.Fubini_integral) (auto simp: indicator_times split_beta')
     also have "\<dots> = (CLINT x | M n. (if x = 0 then 0 else 2 * (u  - sin (u * x) / x)))"
-      using \<open>u > 0\<close> by (intro integral_cong, auto simp add: * simp del: of_real_mult)
+      using \<open>u > 0\<close> by (intro Bochner_Integration.integral_cong, auto simp add: * simp del: of_real_mult)
     also have "\<dots> = (LINT x | M n. (if x = 0 then 0 else 2 * (u  - sin (u * x) / x)))"
       by (rule integral_complex_of_real)
     finally have "Re (CLBINT t:{-u..u}. 1 - char (M n) t) =