do translation: CONST;
authorwenzelm
Fri, 13 Apr 2007 21:26:34 +0200
changeset 22664 e965391e2864
parent 22663 73517244fc46
child 22665 cf152ff55d16
do translation: CONST;
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