diff -r 5e50a2b52809 -r d67dadd69d07 src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Mon Jan 27 20:29:02 2025 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Mon Jan 27 21:31:02 2025 +0100
@@ -1092,7 +1092,7 @@
   "bind M f = (if space M = {} then count_space {} else
     join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f))"
 
-adhoc_overloading Monad_Syntax.bind bind
+adhoc_overloading Monad_Syntax.bind \<rightleftharpoons> bind
 
 lemma bind_empty:
   "space M = {} \<Longrightarrow> bind M f = count_space {}"