escape UTF8 symbols for the ML compiler;

--- a/src/Pure/General/symbol.ML	Thu Jun 24 21:57:18 2010 +0200
+++ b/src/Pure/General/symbol.ML	Thu Jun 24 22:58:45 2010 +0200
@@ -491,7 +491,11 @@
 
 (* escape *)
 
-val esc = fn s => if is_char s then s else "\\" ^ s;
+val esc = fn s =>
+  if is_char s then s
+  else if is_utf8 s then translate_string (fn c => "\\" ^ string_of_int (ord c)) s
+  else "\\" ^ s;
+
 val escape = implode o map esc o sym_explode;