export add_tvarsT, add_tvars, add_vars, add_frees (would actually
belong to term.ML, but is apt to cause some confusion with the
fold-right versions there);

--- a/src/Pure/drule.ML	Mon Nov 05 20:56:29 2001 +0100
+++ b/src/Pure/drule.ML	Mon Nov 05 20:58:28 2001 +0100
@@ -110,6 +110,10 @@
   val implies_intr_goals: cterm list -> thm -> thm
   val freeze_all: thm -> thm
   val mk_triv_goal: cterm -> thm
+  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 tvars_of_terms: term list -> (indexname * sort) list
   val vars_of_terms: term list -> (indexname * typ) list
   val tvars_of: thm -> (indexname * sort) list
@@ -782,6 +786,7 @@
 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);
 
 fun tvars_of_terms ts = rev (foldl add_tvars ([], ts));
 fun vars_of_terms ts = rev (foldl add_vars ([], ts));