diff -r a5c0d61ce5db -r ae2074acbaa8 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Sun Oct 28 16:31:13 2018 +0100
+++ b/src/Tools/Code/code_ml.ML	Tue Oct 30 15:45:24 2018 +0100
@@ -55,7 +55,7 @@
   if c = "\\"
   then "\\092" (*produce strings suitable for both SML as well as Isabelle/ML*)
   else if Symbol.is_ascii c
-  then ML_Syntax.print_char c
+  then ML_Syntax.print_symbol_char c
   else error "non-ASCII byte in SML string literal";
 
 val print_sml_string = quote o translate_string print_sml_char;