# HG changeset patch
# User haftmann
# Date 1279103264 -7200
# Node ID e550439d4422d136761a073e3b4b4ce96fa6e307
# Parent  053d23f089464f5f1089fabf99997048b963a0f8
dropped M suffix; added predicate monad bind

diff -r 053d23f08946 -r e550439d4422 src/HOL/Imperative_HOL/Heap_Monad.thy
--- 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"
diff -r 053d23f08946 -r e550439d4422 src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy	Wed Jul 14 12:27:43 2010 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy	Wed Jul 14 12:27:44 2010 +0200
@@ -15,21 +15,21 @@
 *}
 
 consts
-  bindM :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
+  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
 
 notation (xsymbols)
-  bindM (infixr "\<guillemotright>=" 54)
+  bind (infixr "\<guillemotright>=" 54)
 
 abbreviation (do_notation)
-  bindM_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
+  bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
 where
-  "bindM_do \<equiv> bindM"
+  "bind_do \<equiv> bind"
 
 notation (output)
-  bindM_do (infixr ">>=" 54)
+  bind_do (infixr ">>=" 54)
 
 notation (xsymbols output)
-  bindM_do (infixr "\<guillemotright>=" 54)
+  bind_do (infixr "\<guillemotright>=" 54)
 
 nonterminals
   do_binds do_bind
@@ -49,9 +49,9 @@
 
 translations
   "_do_block (_do_cons (_do_then t) (_do_final e))"
-    == "CONST bindM_do t (\<lambda>_. e)"
+    == "CONST bind_do t (\<lambda>_. e)"
   "_do_block (_do_cons (_do_bind p t) (_do_final e))"
-    == "CONST bindM_do t (\<lambda>p. e)"
+    == "CONST bind_do t (\<lambda>p. e)"
   "_do_block (_do_cons (_do_let p t) bs)"
     == "let p = t in _do_block bs"
   "_do_block (_do_cons b (_do_cons c cs))"
@@ -61,6 +61,9 @@
   "_do_block (_do_final e)" => "e"
   "(m >> n)" => "(m >>= (\<lambda>_. n))"
 
-setup {* Adhoc_Overloading.add_overloaded @{const_name bindM} *}
+setup {*
+  Adhoc_Overloading.add_overloaded @{const_name bind}
+  #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
+*}
 
 end