# HG changeset patch
# User wenzelm
# Date 1004990308 -3600
# Node ID a96c9563d568a21f670d14cbff476c9358635b29
# Parent  7e2e84e503ce05589e81dde0c963f5911fae9c67
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);

diff -r 7e2e84e503ce -r a96c9563d568 src/Pure/drule.ML
--- 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));