1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Jul 14 12:27:43 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Jul 14 12:27:44 2010 +0200
     1.3 @@ -266,10 +266,9 @@
     1.4  
     1.5  setup {*
     1.6    Adhoc_Overloading.add_variant 
     1.7 -    @{const_name Monad_Syntax.bindM} @{const_name Heap_Monad.bind}
     1.8 +    @{const_name Monad_Syntax.bind} @{const_name Heap_Monad.bind}
     1.9  *}
    1.10  
    1.11 -
    1.12  lemma execute_bind [execute_simps]:
    1.13    "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
    1.14    "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"