# HG changeset patch
# User wenzelm
# Date 1176492394 -7200
# Node ID e965391e28646bd2991f8fad6018613f35b6a1e0
# Parent  73517244fc46a032a8e40acfc98f6b5cceaf6453
do translation: CONST;

diff -r 73517244fc46 -r e965391e2864 src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Fri Apr 13 20:23:18 2007 +0200
+++ b/src/HOL/Library/State_Monad.thy	Fri Apr 13 21:26:34 2007 +0200
@@ -218,7 +218,7 @@
     ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
 
 translations
-  "_do f" => "State_Monad.run f"
+  "_do f" => "CONST run f"
   "_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
   "_fcomp f g" => "f \<guillemotright> g"
   "_let x t f" => "Let t (\<lambda>x. f)"
@@ -307,4 +307,4 @@
   For an example, see HOL/ex/CodeRandom.thy (more examples coming soon).
 *}
 
-end
\ No newline at end of file
+end