--- 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 =
--- 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. **)