src/Pure/drule.ML
changeset 8605 625fbbe5c6b4
parent 8550 b44c185f8018
child 9288 06a55195741b
     1.1 --- a/src/Pure/drule.ML	Wed Mar 29 15:09:51 2000 +0200
     1.2 +++ b/src/Pure/drule.ML	Thu Mar 30 14:15:41 2000 +0200
     1.3 @@ -98,6 +98,7 @@
     1.4    val vars_of           : thm -> (indexname * typ) list
     1.5    val unvarifyT         : thm -> thm
     1.6    val unvarify          : thm -> thm
     1.7 +  val tvars_intr_list	: string list -> thm -> thm
     1.8    val rule_attribute    : ('a -> thm -> thm) -> 'a attribute
     1.9    val tag_rule          : tag -> thm -> thm
    1.10    val untag_rule        : string -> thm -> thm
    1.11 @@ -693,6 +694,16 @@
    1.12    in instantiate' [] frees thm end;
    1.13  
    1.14  
    1.15 +(* tvars_intr_list *)
    1.16 +
    1.17 +fun tfrees_of thm =
    1.18 +  let val {hyps, prop, ...} = Thm.rep_thm thm
    1.19 +  in foldr Term.add_term_tfree_names (prop :: hyps, []) end;
    1.20 +
    1.21 +fun tvars_intr_list tfrees thm =
    1.22 +  Thm.varifyT' (tfrees_of thm \\ tfrees) thm;
    1.23 +
    1.24 +
    1.25  (* increment var indexes *)
    1.26  
    1.27  fun incr_indexes 0 thm = thm