# HG changeset patch
# User wenzelm
# Date 1083442137 -7200
# Node ID 9c78044b99c3481346bfb08dc37133d2dfd9ec15
# Parent  49873d345a3962fb36dab34e6150cac45054c712
improved Term.invent_names;

diff -r 49873d345a39 -r 9c78044b99c3 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat May 01 22:07:16 2004 +0200
+++ b/src/Pure/Isar/locale.ML	Sat May 01 22:08:57 2004 +0200
@@ -476,7 +476,7 @@
   let
     val tvars = rev (foldl Term.add_tvarsT ([], Ts));
     val tfrees = map TFree
-      (Term.invent_type_names (ProofContext.used_types ctxt) (length tvars) ~~ map #2 tvars);
+      (Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars);
   in map #1 tvars ~~ tfrees end;
 
 fun unify_frozen ctxt maxidx Ts Us =
diff -r 49873d345a39 -r 9c78044b99c3 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat May 01 22:07:16 2004 +0200
+++ b/src/Pure/axclass.ML	Sat May 01 22:08:57 2004 +0200
@@ -96,7 +96,7 @@
 
 fun mk_arity (t, Ss, c) =
   let
-    val tfrees = ListPair.map TFree (Term.invent_type_names [] (length Ss), Ss);
+    val tfrees = ListPair.map TFree (Term.invent_names [] "'a" (length Ss), Ss);
   in Logic.mk_inclass (Type (t, tfrees), c) end;
 
 fun mk_arities (t, Ss, S) = map (fn c => mk_arity (t, Ss, c)) S;
diff -r 49873d345a39 -r 9c78044b99c3 src/Pure/term.ML
--- a/src/Pure/term.ML	Sat May 01 22:07:16 2004 +0200
+++ b/src/Pure/term.ML	Sat May 01 22:08:57 2004 +0200
@@ -181,7 +181,6 @@
   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   val rename_abs: term -> term -> term -> term option
   val invent_names: string list -> string -> int -> string list
-  val invent_type_names: string list -> int -> string list
   val add_tvarsT: (indexname * sort) list * typ -> (indexname * sort) list
   val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
   val add_vars: (indexname * typ) list * term -> (indexname * typ) list
@@ -773,8 +772,13 @@
       let val b' = variant used b
       in  b' :: variantlist (bs, b'::used)  end;
 
-fun invent_names used prfx n = variantlist (Library.replicate n prfx, prfx :: used);
-fun invent_type_names used = invent_names used "'";
+(*Invent fresh names*)
+fun invent_names _ _ 0 = []
+  | invent_names used a n =
+      let val b = Symbol.bump_string a in
+        if a mem_string used then invent_names used b n
+        else a :: invent_names used b (n - 1)
+      end;
 
 
 
diff -r 49873d345a39 -r 9c78044b99c3 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Sat May 01 22:07:16 2004 +0200
+++ b/src/Pure/type_infer.ML	Sat May 01 22:08:57 2004 +0200
@@ -227,11 +227,6 @@
 
 (* typs_terms_of *)                             (*DESTRUCTIVE*)
 
-fun gen_names 0 _ _ = []
-  | gen_names i s used = if s mem used
-      then gen_names i (Symbol.bump_string s) used
-      else s :: gen_names (i-1) (Symbol.bump_string s) used;
-
 fun typs_terms_of used mk_var prfx (Ts, ts) =
   let
     fun elim (r as ref (Param S), x) = r := mk_var (x, S)
@@ -239,7 +234,7 @@
 
     val used' = foldl add_names (foldl add_namesT (used, Ts), ts);
     val parms = rev (foldl add_parms (foldl add_parmsT ([], Ts), ts));
-    val names = gen_names (length parms) (prfx ^ "'a") used';
+    val names = Term.invent_names used' (prfx ^ "'a") (length parms);
   in
     seq2 elim (parms, names);
     (map simple_typ_of Ts, map simple_term_of ts)