export add_tvarsT, add_tvars, add_vars, add_frees (would actually
authorwenzelm
Mon Nov 05 20:58:28 2001 +0100 (2001-11-05)
changeset 12054a96c9563d568
parent 12053 7e2e84e503ce
child 12055 a9c44895cc8c
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);
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Mon Nov 05 20:56:29 2001 +0100
     1.2 +++ b/src/Pure/drule.ML	Mon Nov 05 20:58:28 2001 +0100
     1.3 @@ -110,6 +110,10 @@
     1.4    val implies_intr_goals: cterm list -> thm -> thm
     1.5    val freeze_all: thm -> thm
     1.6    val mk_triv_goal: cterm -> thm
     1.7 +  val add_tvarsT: (indexname * sort) list * typ -> (indexname * sort) list
     1.8 +  val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
     1.9 +  val add_vars: (indexname * typ) list * term -> (indexname * typ) list
    1.10 +  val add_frees: (string * typ) list * term -> (string * typ) list
    1.11    val tvars_of_terms: term list -> (indexname * sort) list
    1.12    val vars_of_terms: term list -> (indexname * typ) list
    1.13    val tvars_of: thm -> (indexname * sort) list
    1.14 @@ -782,6 +786,7 @@
    1.15  val add_tvarsT = foldl_atyps (fn (vs, TVar v) => v ins vs | (vs, _) => vs);
    1.16  val add_tvars = foldl_types add_tvarsT;
    1.17  val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs | (vs, _) => vs);
    1.18 +val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
    1.19  
    1.20  fun tvars_of_terms ts = rev (foldl add_tvars ([], ts));
    1.21  fun vars_of_terms ts = rev (foldl add_vars ([], ts));