# HG changeset patch
# User Christian Sternagel
# Date 1376987651 -32400
# Node ID ff37dc246b1012cf5970849e065a2c3b94c42f64
# Parent  f557a4645f611d96ac08227e06c4a0b1ba5b9d51
more general typing of monadic bind

diff -r f557a4645f61 -r ff37dc246b10 src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy	Fri Sep 13 09:31:45 2013 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy	Tue Aug 20 17:34:11 2013 +0900
@@ -15,7 +15,7 @@
 *}
 
 consts
-  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
+  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr ">>=" 54)
 
 notation (xsymbols)
   bind (infixr "\<guillemotright>=" 54)
@@ -24,7 +24,7 @@
   bind (infixr "\<bind>" 54)
 
 abbreviation (do_notation)
-  bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
+  bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd"
 where
   "bind_do \<equiv> bind"
 
@@ -46,14 +46,14 @@
   "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
   "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
   "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
-  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr ">>" 54)
+  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
 
 syntax (xsymbols)
   "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ \<leftarrow>/ _)" 13)
-  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<guillemotright>" 54)
+  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<guillemotright>" 54)
 
 syntax (latex output)
-  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<then>" 54)
+  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<then>" 54)
 
 translations
   "_do_block (_do_cons (_do_then t) (_do_final e))"