# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1653472627 -3600
# Node ID 8e2285baadba7faea98ca1be44f518f18d97f33a
# Parent  7448423e5dbaa63a6acc97828810bdd3af9f0874
qualified name to fix integrable_cong ambiguity

diff -r 7448423e5dba -r 8e2285baadba src/HOL/Probability/Levy.thy
--- a/src/HOL/Probability/Levy.thy	Tue May 24 16:21:49 2022 +0100
+++ b/src/HOL/Probability/Levy.thy	Wed May 25 10:57:07 2022 +0100
@@ -350,7 +350,7 @@
       hence "complex_integrable (M n) (\<lambda>x. if x = 0 then 0 else 2 * (u  - sin (u * x) / x))"
         using \<open>u > 0\<close>
         unfolding set_integrable_def
-        by (subst integrable_cong) (auto simp add: * simp del: of_real_mult)
+        by (subst Bochner_Integration.integrable_cong) (auto simp add: * simp del: of_real_mult)
       hence **: "integrable (M n) (\<lambda>x. if x = 0 then 0 else 2 * (u  - sin (u * x) / x))"
         unfolding complex_of_real_integrable_eq .
       have "2 * sin x \<le> x" if "2 \<le> x" for x :: real