diff -r 1d43f86f48be -r e96292f32c3c src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Library/State_Monad.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -118,14 +118,14 @@
 
 syntax
   "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2  _)//}" [12] 62)
-  "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
+  "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13)
   "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(2let _ =/ _)" [1000, 13] 13)
   "_sdo_then" :: "'a \<Rightarrow> sdo_bind" ("_" [14] 13)
   "_sdo_final" :: "'a \<Rightarrow> sdo_binds" ("_")
   "_sdo_cons" :: "[sdo_bind, sdo_binds] \<Rightarrow> sdo_binds" ("_;//_" [13, 12] 12)
 
-syntax (xsymbols)
-  "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13)
+syntax (ASCII)
+  "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
 
 translations
   "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))"