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