1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Jul 25 16:43:47 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Jul 25 16:51:26 2006 +0200
     1.3 @@ -364,7 +364,7 @@
     1.4        in ClassPackage.assume_arities_of_sort thy arities (ty, sort) end;
     1.5      fun mk_cons tyco (c, tys) =
     1.6        let
     1.7 -        val ts = Name.give_names Name.context "a" tys;
     1.8 +        val ts = Name.names Name.context "a" tys;
     1.9          val ty = tys ---> Type (tyco, map TFree vs);
    1.10        in list_comb (Const (c, ty), map Free ts) end;
    1.11    in if forall (fn (_, cs) => forall (fn (_, tys) => forall typ_of_sort tys) cs) css
    1.12 @@ -379,7 +379,7 @@
    1.13      | SOME insts => let
    1.14          fun proven ((tyco, asorts), sort) =
    1.15            Sorts.of_sort (Sign.classes_of thy)
    1.16 -            (Type (tyco, map TFree (Name.give_names Name.context "'a" asorts)), sort);
    1.17 +            (Type (tyco, map TFree (Name.names Name.context "'a" asorts)), sort);
    1.18          val (arities, css) = (split_list o map_filter
    1.19            (fn (tyco, (arity, cs)) => if proven arity
    1.20              then NONE else SOME (arity, (tyco, cs)))) insts;
    1.21 @@ -395,7 +395,7 @@
    1.22  
    1.23  fun dest_case_app cs ts tys =
    1.24    let
    1.25 -    val abs = Name.give_names Name.context "a" (Library.drop (length ts, tys));
    1.26 +    val abs = Name.names Name.context "a" (Library.drop (length ts, tys));
    1.27      val (ts', t) = split_last (ts @ map Free abs);
    1.28      val (tys', sty) = split_last tys;
    1.29      fun freenames_of t = fold_aterms

     2.1 --- a/src/Pure/General/symbol.ML	Tue Jul 25 16:43:47 2006 +0200
     2.2 +++ b/src/Pure/General/symbol.ML	Tue Jul 25 16:51:26 2006 +0200
     2.3 @@ -60,6 +60,7 @@
     2.4    val default_raw: string -> string
     2.5    val xsymbolsN: string
     2.6    val symbol_output: string -> string * real
     2.7 +  val alphanum: string -> string
     2.8  end;
     2.9  
    2.10  structure Symbol: SYMBOL =
    2.11 @@ -516,6 +517,26 @@
    2.12      in (implode (map out syms), real (sym_length syms)) end;
    2.13  
    2.14  
    2.15 +(*turning arbitrary names into alphanumerics*)
    2.16 +
    2.17 +fun alphanum s =
    2.18 +  let
    2.19 +    fun replace_invalid c (last_inv, cs) =
    2.20 +      if ((Char.isAlphaNum o the o Char.fromString) c orelse c = "'")
    2.21 +        andalso not ("." = c)
    2.22 +      then (false, if last_inv then c :: "_" :: cs else c :: cs)
    2.23 +      else (true, cs);
    2.24 +    fun prefix_num_empty [] = ["x"]
    2.25 +      | prefix_num_empty (cs as c::_) =
    2.26 +          if (Char.isDigit o the o Char.fromString) c
    2.27 +          then "x" :: cs
    2.28 +          else cs;
    2.29 +    val (prefix, cs1) = case explode s of "'"::cs => ("'", cs) | cs => ("", cs);
    2.30 +    val (_, cs2) = fold_rev replace_invalid cs1 (false, []);
    2.31 +    val cs3 = prefix_num_empty cs2;
    2.32 +  in implode (prefix :: cs3) end;
    2.33 +
    2.34 +
    2.35  (*final declarations of this structure!*)
    2.36  val length = sym_length;
    2.37  val explode = sym_explode;

     3.1 --- a/src/Pure/Tools/class_package.ML	Tue Jul 25 16:43:47 2006 +0200
     3.2 +++ b/src/Pure/Tools/class_package.ML	Tue Jul 25 16:51:26 2006 +0200
     3.3 @@ -461,7 +461,7 @@
     3.4        end;
     3.5      fun get_consts_sort (tyco, asorts, sort) =
     3.6        let
     3.7 -        val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) (Name.give_names Name.context "'a" asorts))
     3.8 +        val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) (Name.names Name.context "'a" asorts))
     3.9        in maps (get_consts_class tyco ty) (the_ancestry theory sort) end;
    3.10      val cs = maps get_consts_sort arities;
    3.11      fun read_defs defs cs thy_read =

     4.1 --- a/src/Pure/Tools/codegen_package.ML	Tue Jul 25 16:43:47 2006 +0200
     4.2 +++ b/src/Pure/Tools/codegen_package.ML	Tue Jul 25 16:51:26 2006 +0200
     4.3 @@ -756,7 +756,7 @@
     4.4        |-> (fn ty => pair (IVar v))
     4.5    | exprgen_term thy tabs (Abs (raw_v, ty, raw_t)) trns =
     4.6        let
     4.7 -        val (v, t) = Term.variant_abs (Name.alphanum raw_v, ty, raw_t);
     4.8 +        val (v, t) = Term.variant_abs (Symbol.alphanum raw_v, ty, raw_t);
     4.9        in
    4.10          trns
    4.11          |> exprgen_type thy tabs ty
    4.12 @@ -792,7 +792,7 @@
    4.13          if length ts < i then
    4.14            let
    4.15              val tys = Library.take (i - length ts, ((fst o strip_type) ty));
    4.16 -            val vs = Name.give_names (Name.declare f Name.context) "a" tys;
    4.17 +            val vs = Name.names (Name.declare f Name.context) "a" tys;
    4.18            in
    4.19              trns
    4.20              |> fold_map (exprgen_type thy tabs) tys

     5.1 --- a/src/Pure/Tools/codegen_serializer.ML	Tue Jul 25 16:43:47 2006 +0200
     5.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Tue Jul 25 16:51:26 2006 +0200
     5.3 @@ -343,9 +343,9 @@
     5.4    type src = string;
     5.5    val ord = string_ord;
     5.6    fun mk reserved_ml (name, 0) =
     5.7 -        (Name.alphanum o NameSpace.base) name
     5.8 +        (Symbol.alphanum o NameSpace.base) name
     5.9      | mk reserved_ml (name, i) =
    5.10 -        (Name.alphanum o NameSpace.base) name ^ replicate_string i "'";
    5.11 +        (Symbol.alphanum o NameSpace.base) name ^ replicate_string i "'";
    5.12    fun is_valid (reserved_ml : string list) = not o member (op =) reserved_ml;
    5.13    fun maybe_unique _ _ = NONE;
    5.14    fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);

     6.1 --- a/src/Pure/Tools/codegen_theorems.ML	Tue Jul 25 16:43:47 2006 +0200
     6.2 +++ b/src/Pure/Tools/codegen_theorems.ML	Tue Jul 25 16:51:26 2006 +0200
     6.3 @@ -225,7 +225,7 @@
     6.4              (ctyp_of thy ty, ctyp_of thy (TVar ((v', maxidx), sort))) :: acc)
     6.5          end;
     6.6      val lower_name = implode o map (Char.toString o Char.toLower o the o Char.fromString)
     6.7 -      o explode o Name.alphanum;
     6.8 +      o explode o Symbol.alphanum;
     6.9      fun tvars_of thm = (fold_types o fold_atyps)
    6.10        (fn TVar (v_i as (v, i), sort) => cons (v_i, (lower_name v, sort))
    6.11          | _ => I) (prop_of thm) [];
    6.12 @@ -244,7 +244,7 @@
    6.13              (cterm_of thy t, cterm_of thy (Var ((v', maxidx), ty))) :: acc)
    6.14          end;
    6.15      val lower_name = implode o map (Char.toString o Char.toLower o the o Char.fromString)
    6.16 -      o explode o Name.alphanum;
    6.17 +      o explode o Symbol.alphanum;
    6.18      fun vars_of thm = fold_aterms
    6.19        (fn Var (v_i as (v, i), ty) => cons (v_i, (lower_name v, ty))
    6.20          | _ => I) (prop_of thm) [];

     7.1 --- a/src/Pure/Tools/codegen_thingol.ML	Tue Jul 25 16:43:47 2006 +0200
     7.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Tue Jul 25 16:51:26 2006 +0200
     7.3 @@ -370,7 +370,7 @@
     7.4      val j = length es;
     7.5      val l = k - j;
     7.6      val tys = (curry Library.take l o curry Library.drop j o fst o unfold_fun) ty;
     7.7 -    val vs_tys = Name.give_names (fold Name.declare (fold add_varnames es []) Name.context) "a" tys;
     7.8 +    val vs_tys = Name.names (fold Name.declare (fold add_varnames es []) Name.context) "a" tys;
     7.9    in vs_tys `|--> IConst c `$$ es @ map (fn (v, _) => IVar v) vs_tys end;
    7.10  
    7.11  

     8.1 --- a/src/Pure/name.ML	Tue Jul 25 16:43:47 2006 +0200
     8.2 +++ b/src/Pure/name.ML	Tue Jul 25 16:51:26 2006 +0200
     8.3 @@ -21,12 +21,11 @@
     8.4    val declare: string -> context -> context
     8.5    val is_declared: context -> string -> bool
     8.6    val invents: context -> string -> int -> string list
     8.7 -  val give_names: context -> string -> 'a list -> (string * 'a) list
     8.8 +  val names: context -> string -> 'a list -> (string * 'a) list
     8.9    val invent_list: string list -> string -> int -> string list
    8.10    val variants: string list -> context -> string list * context
    8.11    val variant_list: string list -> string list -> string list
    8.12    val variant: string list -> string -> string
    8.13 -  val alphanum: string -> string
    8.14  end;
    8.15  
    8.16  structure Name: NAME =
    8.17 @@ -101,7 +100,7 @@
    8.18    in invs o clean end;
    8.19  
    8.20  val invent_list = invents o make_context;
    8.21 -fun give_names ctxt x xs = invents ctxt x (length xs) ~~ xs;
    8.22 +fun names ctxt x xs = invents ctxt x (length xs) ~~ xs;
    8.23  
    8.24  
    8.25  (* variants *)
    8.26 @@ -131,24 +130,4 @@
    8.27  fun variant_list used names = #1 (make_context used |> variants names);
    8.28  fun variant used = singleton (variant_list used);
    8.29  
    8.30 -
    8.31 -(*turning arbitrary names into alphanumerics*)
    8.32 -
    8.33 -fun alphanum s =
    8.34 -  let
    8.35 -    fun replace_invalid c (last_inv, cs) =
    8.36 -      if ((Char.isAlphaNum o the o Char.fromString) c orelse c = "'")
    8.37 -        andalso not (NameSpace.separator = c)
    8.38 -      then (false, if last_inv then c :: "_" :: cs else c :: cs)
    8.39 -      else (true, cs);
    8.40 -    fun prefix_num_empty [] = ["x"]
    8.41 -      | prefix_num_empty (cs as c::_) =
    8.42 -          if (Char.isDigit o the o Char.fromString) c
    8.43 -          then "x" :: cs
    8.44 -          else cs;
    8.45 -    val (prefix, cs1) = case explode s of "'"::cs => ("'", cs) | cs => ("", cs);
    8.46 -    val (_, cs2) = fold_rev replace_invalid cs1 (false, []);
    8.47 -    val cs3 = prefix_num_empty cs2;
    8.48 -  in implode (prefix :: cs3) end;
    8.49 -
    8.50  end;