--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Jul 14 12:27:43 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Jul 14 12:27:44 2010 +0200
@@ -266,10 +266,9 @@
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"