1.1 --- a/src/HOL/Library/Monad_Syntax.thy	Fri Sep 13 09:31:45 2013 +0200
     1.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Tue Aug 20 17:34:11 2013 +0900
     1.3 @@ -15,7 +15,7 @@
     1.4  *}
     1.5  
     1.6  consts
     1.7 -  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
     1.8 +  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr ">>=" 54)
     1.9  
    1.10  notation (xsymbols)
    1.11    bind (infixr "\<guillemotright>=" 54)
    1.12 @@ -24,7 +24,7 @@
    1.13    bind (infixr "\<bind>" 54)
    1.14  
    1.15  abbreviation (do_notation)
    1.16 -  bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
    1.17 +  bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd"
    1.18  where
    1.19    "bind_do \<equiv> bind"
    1.20  
    1.21 @@ -46,14 +46,14 @@
    1.22    "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
    1.23    "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
    1.24    "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
    1.25 -  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr ">>" 54)
    1.26 +  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
    1.27  
    1.28  syntax (xsymbols)
    1.29    "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ \<leftarrow>/ _)" 13)
    1.30 -  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<guillemotright>" 54)
    1.31 +  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<guillemotright>" 54)
    1.32  
    1.33  syntax (latex output)
    1.34 -  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<then>" 54)
    1.35 +  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<then>" 54)
    1.36  
    1.37  translations
    1.38    "_do_block (_do_cons (_do_then t) (_do_final e))"