diff -r d30f4a509361 -r 23ce0d32de11 src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Wed Mar 12 08:47:35 2008 +0100
+++ b/src/HOL/Library/State_Monad.thy	Wed Mar 12 08:47:36 2008 +0100
@@ -115,8 +115,8 @@
   \begin{itemize}
     \item The monad model does not state anything about
        the kind of state; the model for the state is
-       completely orthogonal and has to (or may) be
-       specified completely independent.
+       completely orthogonal and may be
+       specified completely independently.
     \item There is no distinguished type constructor
        encapsulating away the state transformation, i.e.~transformations
        may be applied directly without using any lifting
@@ -191,6 +191,26 @@
 lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp
   mbind_def fcomp_def run_def
 
+subsection {* ML abstract operations *}
+
+ML {*
+structure StateMonad =
+struct
+
+fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
+fun liftT' sT = sT --> sT;
+
+fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
+
+fun mbind T1 T2 sT f g = Const (@{const_name mbind},
+  liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
+
+fun run T sT f = Const (@{const_name run}, liftT' (liftT T sT)) $ f;
+
+end;
+*}
+
+
 subsection {* Syntax *}
 
 text {*
@@ -270,8 +290,7 @@
 | "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
 
 definition
-  collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a"
-  where
+  collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
   "collapse f = (do g \<leftarrow> f; g done)"
 
 text {* combinator properties *}