--- a/src/Pure/drule.ML Wed Mar 29 15:09:51 2000 +0200
+++ b/src/Pure/drule.ML Thu Mar 30 14:15:41 2000 +0200
@@ -98,6 +98,7 @@
val vars_of : thm -> (indexname * typ) list
val unvarifyT : thm -> thm
val unvarify : thm -> thm
+ val tvars_intr_list : string list -> thm -> thm
val rule_attribute : ('a -> thm -> thm) -> 'a attribute
val tag_rule : tag -> thm -> thm
val untag_rule : string -> thm -> thm
@@ -693,6 +694,16 @@
in instantiate' [] frees thm end;
+(* tvars_intr_list *)
+
+fun tfrees_of thm =
+ let val {hyps, prop, ...} = Thm.rep_thm thm
+ in foldr Term.add_term_tfree_names (prop :: hyps, []) end;
+
+fun tvars_intr_list tfrees thm =
+ Thm.varifyT' (tfrees_of thm \\ tfrees) thm;
+
+
(* increment var indexes *)
fun incr_indexes 0 thm = thm