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"

     2.1 --- a/src/HOL/Library/Monad_Syntax.thy	Wed Jul 14 12:27:43 2010 +0200
     2.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Wed Jul 14 12:27:44 2010 +0200
     2.3 @@ -15,21 +15,21 @@
     2.4  *}
     2.5  
     2.6  consts
     2.7 -  bindM :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
     2.8 +  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
     2.9  
    2.10  notation (xsymbols)
    2.11 -  bindM (infixr "\<guillemotright>=" 54)
    2.12 +  bind (infixr "\<guillemotright>=" 54)
    2.13  
    2.14  abbreviation (do_notation)
    2.15 -  bindM_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
    2.16 +  bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
    2.17  where
    2.18 -  "bindM_do \<equiv> bindM"
    2.19 +  "bind_do \<equiv> bind"
    2.20  
    2.21  notation (output)
    2.22 -  bindM_do (infixr ">>=" 54)
    2.23 +  bind_do (infixr ">>=" 54)
    2.24  
    2.25  notation (xsymbols output)
    2.26 -  bindM_do (infixr "\<guillemotright>=" 54)
    2.27 +  bind_do (infixr "\<guillemotright>=" 54)
    2.28  
    2.29  nonterminals
    2.30    do_binds do_bind
    2.31 @@ -49,9 +49,9 @@
    2.32  
    2.33  translations
    2.34    "_do_block (_do_cons (_do_then t) (_do_final e))"
    2.35 -    == "CONST bindM_do t (\<lambda>_. e)"
    2.36 +    == "CONST bind_do t (\<lambda>_. e)"
    2.37    "_do_block (_do_cons (_do_bind p t) (_do_final e))"
    2.38 -    == "CONST bindM_do t (\<lambda>p. e)"
    2.39 +    == "CONST bind_do t (\<lambda>p. e)"
    2.40    "_do_block (_do_cons (_do_let p t) bs)"
    2.41      == "let p = t in _do_block bs"
    2.42    "_do_block (_do_cons b (_do_cons c cs))"
    2.43 @@ -61,6 +61,9 @@
    2.44    "_do_block (_do_final e)" => "e"
    2.45    "(m >> n)" => "(m >>= (\<lambda>_. n))"
    2.46  
    2.47 -setup {* Adhoc_Overloading.add_overloaded @{const_name bindM} *}
    2.48 +setup {*
    2.49 +  Adhoc_Overloading.add_overloaded @{const_name bind}
    2.50 +  #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
    2.51 +*}
    2.52  
    2.53  end