# HG changeset patch
# User wenzelm
# Date 954418541 -7200
# Node ID 625fbbe5c6b4b0c6d12aaf4f83005d0adc51baf3
# Parent  c99e0024050c5cde004d4e8d37482a17be3f6b9f
added tvars_intr_list;

diff -r c99e0024050c -r 625fbbe5c6b4 src/Pure/drule.ML
--- 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