src/HOL/Imperative_HOL/Heap_Monad.thy

                   Some (x, h') \<Rightarrow> execute (g x) h'
                 | None \<Rightarrow> None)"
 
 setup {*
   Adhoc_Overloading.add_variant 
-    @{const_name Monad_Syntax.bindM} @{const_name Heap_Monad.bind}
+    @{const_name Monad_Syntax.bind} @{const_name Heap_Monad.bind}
 *}
-
 
 lemma execute_bind [execute_simps]:
   "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
   "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
   by (simp_all add: bind_def)