avoid structure Char;

--- a/src/Pure/Tools/codegen_serializer.ML	Tue Jul 25 21:18:09 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Tue Jul 25 21:18:11 2006 +0200
@@ -230,8 +230,8 @@
 
 fun abstract_validator keywords name =
   let
-    fun replace_invalid c =
-      if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
+    fun replace_invalid c =  (* FIXME *)
+      if Symbol.is_ascii_letter c orelse Symbol.is_ascii_digit c orelse c = "'"
       andalso not (NameSpace.separator = c)
       then c
       else "_"
@@ -336,16 +336,14 @@
 
 val reserved_ml = ThmDatabase.ml_reserved @ [
   "bool", "int", "list", "unit", "option", "true", "false", "not", "None", "Some", "o"
-];
+];  (* FIXME None/Some no longer used *)
 
 structure NameMangler = NameManglerFun (
   type ctxt = string list;
   type src = string;
   val ord = string_ord;
-  fun mk reserved_ml (name, 0) =
-        (Symbol.alphanum o NameSpace.base) name
-    | mk reserved_ml (name, i) =
-        (Symbol.alphanum o NameSpace.base) name ^ replicate_string i "'";
+  fun mk reserved_ml (name, i) =
+    (Symbol.alphanum o NameSpace.base) name ^ replicate_string i "'";
   fun is_valid (reserved_ml : string list) = not o member (op =) reserved_ml;
   fun maybe_unique _ _ = NONE;
   fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);
@@ -360,7 +358,7 @@
           str "()"
       | ml_from_tyvar (v, sort) =
           let
-            val w = (Char.toString o Char.toUpper o the o Char.fromString) v;
+            val w = Symbol.to_ascii_upper v;
             fun mk_class class =
               str (prefix "'" v ^ " " ^ resolv class);
           in
@@ -400,10 +398,10 @@
               )
           | from_classlookup fxy (Lookup (classes, (v, ~1))) =
               from_lookup BR classes
-                ((str o Char.toString o Char.toUpper o the o Char.fromString) v)
+                ((str o Symbol.to_ascii_upper) v)
           | from_classlookup fxy (Lookup (classes, (v, i))) =
               from_lookup BR (string_of_int (i+1) :: classes)
-                ((str o Char.toString o Char.toUpper o the o Char.fromString) v)
+                ((str o Symbol.to_ascii_upper) v)
       in case lss
        of [] => str "()"
         | [ls] => from_classlookup fxy ls
@@ -471,7 +469,7 @@
           ]
       | ml_from_expr _ (IChar (c, _)) =
           (str o prefix "#" o quote)
-            (let val i = (Char.ord o the o Char.fromString) c
+            (let val i = ord c
               in if i < 32
                 then prefix "\\" (string_of_int i)
                 else c

--- a/src/Pure/Tools/codegen_theorems.ML	Tue Jul 25 21:18:09 2006 +0200
+++ b/src/Pure/Tools/codegen_theorems.ML	Tue Jul 25 21:18:11 2006 +0200
@@ -214,6 +214,8 @@
     |> beta_norm
   end;
 
+val lower_name = translate_string Symbol.to_ascii_lower o Symbol.alphanum;
+
 fun canonical_tvars thy thm =
   let
     fun mk_inst (v_i as (v, i), (v', sort)) (s as (maxidx, set, acc)) =
@@ -224,8 +226,6 @@
           (maxidx + 1, v :: set,
             (ctyp_of thy ty, ctyp_of thy (TVar ((v', maxidx), sort))) :: acc)
         end;
-    val lower_name = implode o map (Char.toString o Char.toLower o the o Char.fromString)
-      o explode o Symbol.alphanum;
     fun tvars_of thm = (fold_types o fold_atyps)
       (fn TVar (v_i as (v, i), sort) => cons (v_i, (lower_name v, sort))
         | _ => I) (prop_of thm) [];
@@ -243,8 +243,6 @@
           (maxidx + 1,  v :: set,
             (cterm_of thy t, cterm_of thy (Var ((v', maxidx), ty))) :: acc)
         end;
-    val lower_name = implode o map (Char.toString o Char.toLower o the o Char.fromString)
-      o explode o Symbol.alphanum;
     fun vars_of thm = fold_aterms
       (fn Var (v_i as (v, i), ty) => cons (v_i, (lower_name v, ty))
         | _ => I) (prop_of thm) [];