src/Pure/General/symbol.ML

 val enc_end = 255;
 
 val enc_vector =
 [
 (* GENERATED TEXT FOLLOWS - Do not edit! *)
-  "\\<space2>",
+  "\\<spacespace>",
   "\\<Gamma>",
   "\\<Delta>",
   "\\<Theta>",
   "\\<Lambda>",
   "\\<Pi>",

   | is_quasi_letter "'" = true
   | is_quasi_letter s = is_letter s;
 
 val is_blank =
   fn " " => true | "\t" => true | "\n" => true | "\^L" => true
-    | "\160" => true | "\\<space2>" => true
+    | "\160" => true | "\\<spacespace>" => true
     | _ => false;
 
 val is_letdig = is_quasi_letter orf is_digit;
 
 fun is_printable s =

   let val chs = explode str in
     if forall (fn c => ord c < enc_start) chs then str
     else implode (map symbol' chs)
   end;
 
-val output = implode o map char o sym_explode;
+fun char' s = if size s > 1 then "\\" ^ s else s;
+fun output s = let val chr = (* if "isabelle_font" mem_string !print_mode *)
+(* FIXME: does not work yet, because of static calls to output in printer.ML *)
+			     (* then *) char (* else char'*)
+		in (implode o map chr o sym_explode) s end;
 
 
 (*final declarations of this structure!*)
 val explode = sym_explode;
 val length = sym_length;