# HG changeset patch
# User wenzelm
# Date 911307947 -3600
# Node ID 5d9beee36fbe90e18f8bae48863bb52145876861
# Parent  c39b23d752b6fe54c38c713afa87b540b88310a9
export vars_of and friends;
open BasicDrule only;

diff -r c39b23d752b6 -r 5d9beee36fbe src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Nov 17 14:04:52 1998 +0100
+++ b/src/Pure/drule.ML	Tue Nov 17 14:05:47 1998 +0100
@@ -8,7 +8,7 @@
 
 infix 0 RS RSN RL RLN MRS MRL COMP;
 
-signature DRULE =
+signature BASIC_DRULE =
 sig
   val dest_implies      : cterm -> cterm * cterm
   val skip_flexpairs	: cterm -> cterm
@@ -73,15 +73,24 @@
   val triv_forall_equality: thm
   val swap_prems_rl     : thm
   val equal_intr_rule   : thm
+  val instantiate'	: ctyp option list -> cterm option list -> thm -> thm
+end;
+
+signature DRULE =
+sig
+  include BASIC_DRULE
   val triv_goal		: thm
   val rev_triv_goal	: thm
   val mk_triv_goal      : cterm -> thm
-  val instantiate'	: ctyp option list -> cterm option list -> thm -> thm
+  val tvars_of_terms	: term list -> (indexname * sort) list
+  val vars_of_terms	: term list -> (indexname * typ) list
+  val tvars_of		: thm -> (indexname * sort) list
+  val vars_of		: thm -> (indexname * typ) list
   val unvarifyT		: thm -> thm
   val unvarify		: thm -> thm
 end;
 
-structure Drule : DRULE =
+structure Drule: DRULE =
 struct
 
 
@@ -601,8 +610,11 @@
 val add_tvars = foldl_types add_tvarsT;
 val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs | (vs, _) => vs);
 
-fun tvars_of thm = rev (add_tvars ([], #prop (Thm.rep_thm thm)));
-fun vars_of thm = rev (add_vars ([], #prop (Thm.rep_thm thm)));
+fun tvars_of_terms ts = rev (foldl add_tvars ([], ts));
+fun vars_of_terms ts = rev (foldl add_vars ([], ts));
+
+fun tvars_of thm = tvars_of_terms [#prop (Thm.rep_thm thm)];
+fun vars_of thm = vars_of_terms [#prop (Thm.rep_thm thm)];
 
 
 (* instantiate by left-to-right occurrence of variables *)
@@ -659,4 +671,6 @@
 
 end;
 
-open Drule;
+
+structure BasicDrule: BASIC_DRULE = Drule;
+open BasicDrule;