diff -r 4d9518c3d031 -r b66d2ca1f907 src/HOL/HOLCF/Sfun.thy
--- a/src/HOL/HOLCF/Sfun.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/Sfun.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -8,12 +8,12 @@
 imports Cfun
 begin
 
-pcpodef ('a, 'b) sfun (infixr "->!" 0)
+pcpodef ('a, 'b) sfun (infixr "\<rightarrow>!" 0)
   = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
 by simp_all
 
-type_notation (xsymbols)
-  sfun  (infixr "\<rightarrow>!" 0)
+type_notation (ASCII)
+  sfun  (infixr "->!" 0)
 
 text {* TODO: Define nice syntax for abstraction, application. *}