# HG changeset patch
# User haftmann
# Date 1279103264 -7200
# Node ID 71e5546b19659497ee6f637cbe7ffdb1369cc54c
# Parent  e550439d4422d136761a073e3b4b4ce96fa6e307
tuned infix syntax

diff -r e550439d4422 -r 71e5546b1965 src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Wed Jul 14 12:27:44 2010 +0200
+++ b/src/HOL/Library/State_Monad.thy	Wed Jul 14 12:27:44 2010 +0200
@@ -56,9 +56,7 @@
 *}
 
 notation fcomp (infixl "\<circ>>" 60)
-notation (xsymbols) fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "o->" 60)
-notation (xsymbols) scomp (infixl "\<circ>\<rightarrow>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 abbreviation (input)
   "return \<equiv> Pair"
@@ -112,10 +110,14 @@
 
 lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
 
+
+subsection {* Do-syntax *}
+
 setup {*
-  Adhoc_Overloading.add_variant @{const_name bindM} @{const_name scomp}
+  Adhoc_Overloading.add_variant @{const_name bind} @{const_name scomp}
 *}
 
+
 text {*
   For an example, see HOL/Extraction/Higman.thy.
 *}