--- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Jan 27 20:29:02 2025 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Mon Jan 27 21:31:02 2025 +0100
@@ -367,7 +367,7 @@
     done
 qed
 
-adhoc_overloading Monad_Syntax.bind bind_pmf
+adhoc_overloading Monad_Syntax.bind \<rightleftharpoons> bind_pmf
 
 lemma ennreal_pmf_bind: "pmf (bind_pmf N f) i = (\<integral>\<^sup>+x. pmf (f x) i \<partial>measure_pmf N)"
   unfolding pmf.rep_eq bind_pmf.rep_eq