diff -r 47050cdc1694 -r a29412af6aa3 src/Pure/General/ml_syntax.ML
--- a/src/Pure/General/ml_syntax.ML	Thu Nov 23 20:33:29 2006 +0100
+++ b/src/Pure/General/ml_syntax.ML	Thu Nov 23 20:33:32 2006 +0100
@@ -47,12 +47,16 @@
 fun str_of_option f NONE = "NONE"
   | str_of_option f (SOME x) = "SOME (" ^ f x ^ ")";
 
-fun str_of_char c =
-  if not (Symbol.is_char c) then raise Fail ("Bad character: " ^ quote c)
-  else if c = "\"" then "\\\""
-  else if c = "\\" then "\\\\"
-  else if Symbol.is_printable c then c
-  else "\\" ^ string_of_int (ord c);
+fun str_of_char s =
+  if not (Symbol.is_char s) then raise Fail ("Bad character: " ^ quote s)
+  else if s = "\"" then "\\\""
+  else if s = "\\" then "\\\\"
+  else
+    let val c = ord s in
+      if c < 32 then "\\^" ^ chr (c + ord "@")
+      else if c < 127 then s
+      else "\\" ^ string_of_int c
+    end;
 
 val str_of_string = quote o translate_string str_of_char;