diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Library/State_Monad.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -68,12 +68,16 @@
 
 definition
   mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
-    (infixl ">>=" 60)
+    (infixl ">>=" 60) where
   "f >>= g = split g \<circ> f"
+
+definition
   fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
-    (infixl ">>" 60)
+    (infixl ">>" 60) where
   "f >> g = g \<circ> f"
-  run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+
+definition
+  run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
   "run f = f"
 
 print_ast_translation {*[