src/Pure/drule.ML
changeset 12495 89f97fa683f5
parent 12373 704e50ab65af
child 12527 d6c91bc3e49c
     1.1 --- a/src/Pure/drule.ML	Fri Dec 14 11:50:38 2001 +0100
     1.2 +++ b/src/Pure/drule.ML	Fri Dec 14 11:51:01 2001 +0100
     1.3 @@ -112,17 +112,13 @@
     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    val vars_of: thm -> (indexname * typ) list
    1.15    val unvarifyT: thm -> thm
    1.16    val unvarify: thm -> thm
    1.17 -  val tvars_intr_list: string list -> thm -> thm
    1.18 +  val tvars_intr_list: string list -> thm -> thm * (string * indexname) list
    1.19    val remdups_rl: thm
    1.20    val conj_intr: thm -> thm -> thm
    1.21    val conj_intr_list: thm list -> thm
    1.22 @@ -794,15 +790,10 @@
    1.23  fun inst x t = read_instantiate_sg (sign_of (the_context())) [(x,t)];
    1.24  
    1.25  
    1.26 -(* collect vars *)
    1.27 +(* collect vars in left-to-right order *)
    1.28  
    1.29 -val add_tvarsT = foldl_atyps (fn (vs, TVar v) => v ins vs | (vs, _) => vs);
    1.30 -val add_tvars = foldl_types add_tvarsT;
    1.31 -val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs | (vs, _) => vs);
    1.32 -val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
    1.33 -
    1.34 -fun tvars_of_terms ts = rev (foldl add_tvars ([], ts));
    1.35 -fun vars_of_terms ts = rev (foldl add_vars ([], ts));
    1.36 +fun tvars_of_terms ts = rev (foldl Term.add_tvars ([], ts));
    1.37 +fun vars_of_terms ts = rev (foldl Term.add_vars ([], ts));
    1.38  
    1.39  fun tvars_of thm = tvars_of_terms [#prop (Thm.rep_thm thm)];
    1.40  fun vars_of thm = vars_of_terms [#prop (Thm.rep_thm thm)];