added write_charnames';

--- a/src/Pure/Syntax/symbol_font.ML	Mon Dec 16 10:03:30 1996 +0100
+++ b/src/Pure/Syntax/symbol_font.ML	Mon Dec 16 10:04:12 1996 +0100
@@ -10,7 +10,8 @@
   val char: string -> string option
   val name: string -> string option
   val read_charnames: string list -> string list
-  val write_charnames:  string list -> string list
+  val write_charnames:  string list -> string list	(*normal backslashes*)
+  val write_charnames':  string list -> string list	(*escaped backslashes*)
 end;
 
 
@@ -76,12 +77,13 @@
 
 (* write_charnames *)
 
-fun write_char ch =
+fun write_char prfx ch =
   (case name ch of
     None => ch
-  | Some nm => "\\<" ^ nm ^ ">");
+  | Some nm => prfx ^ "\\<" ^ nm ^ ">");
 
-val write_charnames = map write_char;
+val write_charnames = map (write_char "");
+val write_charnames' = map (write_char "\\");
 
 
 end;