# HG changeset patch
# User wenzelm
# Date 991324622 -7200
# Node ID 7f6eff7bc97af22528515cd0c019cda1bd975bb3
# Parent  140d55f5836d9b0d75eb483b5e6fb9a15894d75e
invent_names

diff -r 140d55f5836d -r 7f6eff7bc97a src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Thu May 31 17:24:56 2001 +0200
+++ b/src/Pure/axclass.ML	Thu May 31 17:57:02 2001 +0200
@@ -103,8 +103,7 @@
 
 fun mk_arity (t, ss, c) =
   let
-    val names = tl (variantlist (replicate (length ss + 1) "'", []));
-    val tfrees = ListPair.map TFree (names, ss);
+    val tfrees = ListPair.map TFree (Term.invent_names (length ss + 1) "'", ss);
   in Logic.mk_inclass (Type (t, tfrees), c) end;
 
 fun dest_arity tm =
diff -r 140d55f5836d -r 7f6eff7bc97a src/Pure/term.ML
--- a/src/Pure/term.ML	Thu May 31 17:24:56 2001 +0200
+++ b/src/Pure/term.ML	Thu May 31 17:57:02 2001 +0200
@@ -174,6 +174,7 @@
 signature TERM =
 sig
   include BASIC_TERM
+  val invent_names: int -> string -> string list
   val indexname_ord: indexname * indexname -> order
   val typ_ord: typ * typ -> order
   val typs_ord: typ list * typ list -> order
@@ -735,6 +736,8 @@
       let val b' = variant used b
       in  b' :: variantlist (bs, b'::used)  end;
 
+fun invent_names n prfx = Library.tl (variantlist (Library.replicate (n + 1) prfx, []));
+
 
 
 (** Consts etc. **)