src/Tools/Code/code_ml.ML

   | tuplify print fxy [x] = SOME (print fxy x)
   | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
 
 
 (** SML serializer **)
+
+fun print_char_any_ml s =
+  if Symbol.is_char s then ML_Syntax.print_char s else "\\092" ^ unprefix "\\" s;
+
+val print_string_any_ml = quote o implode o map print_char_any_ml o Symbol.explode;
 
 fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
   let
     val deresolve_const = deresolve o Constant;
     val deresolve_class = deresolve o Type_Class;

             :: deresolve_const const
             :: replicate n "_"
             @ "="
             :: "raise"
             :: "Fail"
-            @@ ML_Syntax.print_string const
+            @@ print_string_any_ml const
           ))
       | print_stmt _ (ML_Val binding) =
           let
             val (sig_p, p) = print_def (K false) true "val" binding
           in pair

     @| str ("end; (*struct " ^ name ^ "*)")
   );
 
 val literals_sml = Literals {
   literal_char = prefix "#" o quote o ML_Syntax.print_char,
-  literal_string = quote o translate_string ML_Syntax.print_char,
+  literal_string = print_string_any_ml,
   literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
   literal_list = enum "," "[" "]",
   infix_cons = (7, "::")
 };