# HG changeset patch
# User wenzelm
# Date 1008327211 -3600
# Node ID 1b56e1732a612da9976805a894489f0d4d8f6bdc
# Parent  3b0091bf06e857225ddcc8ea04981a1d5fa63f80
added invent_type_names;
added add_tvarsT etc. (from drule.ML);

diff -r 3b0091bf06e8 -r 1b56e1732a61 src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Dec 14 11:52:54 2001 +0100
+++ b/src/Pure/term.ML	Fri Dec 14 11:53:31 2001 +0100
@@ -175,7 +175,12 @@
 signature TERM =
 sig
   include BASIC_TERM
-  val invent_names: int -> string -> string list
+  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
+  val add_frees: (string * typ) list * term -> (string * typ) list
   val indexname_ord: indexname * indexname -> order
   val typ_ord: typ * typ -> order
   val typs_ord: typ list * typ list -> order
@@ -742,7 +747,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, []));
+fun invent_names used prfx n = variantlist (Library.replicate n prfx, prfx :: used);
+fun invent_type_names used = invent_names used "'";
 
 
 
@@ -934,6 +940,12 @@
 
 fun foldl_types f = foldl_term_types (fn _ => f);
 
+(*collect variables*)
+val add_tvarsT = foldl_atyps (fn (vs, TVar v) => v ins vs | (vs, _) => vs);
+val add_tvars = foldl_types add_tvarsT;
+val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs | (vs, _) => vs);
+val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
+
 
 
 (** type and term orders **)