# HG changeset patch
# User wenzelm
# Date 1112858840 -7200
# Node ID 2b1f1902505dd9a455b0bb2eba3d3f2c0b75efa8
# Parent  53c049a365cf73c0b511b490d2eb65a0a898c18d
added add_used; include tpairs;

diff -r 53c049a365cf -r 2b1f1902505d src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Apr 07 09:27:09 2005 +0200
+++ b/src/Pure/drule.ML	Thu Apr 07 09:27:20 2005 +0200
@@ -86,6 +86,7 @@
   include BASIC_DRULE
   val strip_comb: cterm -> cterm * cterm list
   val strip_type: ctyp -> ctyp list * ctyp
+  val add_used: thm -> string list -> string list
   val rule_attribute: ('a -> thm -> thm) -> 'a attribute
   val tag_rule: tag -> thm -> thm
   val untag_rule: string -> thm -> thm
@@ -252,8 +253,9 @@
 ***)
 
 fun types_sorts thm =
-    let val {prop,hyps,...} = rep_thm thm;
-        val big = list_comb(prop,hyps); (* bogus term! *)
+    let val {prop, hyps, tpairs, ...} = Thm.rep_thm thm;
+        (* bogus term! *)
+        val big = list_comb (list_comb (prop, hyps), Thm.terms_of_tpairs tpairs);
         val vars = map dest_Var (term_vars big);
         val frees = map dest_Free (term_frees big);
         val tvars = term_tvars big;
@@ -262,6 +264,13 @@
         fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i));
     in (typ,sort) end;
 
+fun add_used thm used =
+  let val {prop, hyps, tpairs, ...} = Thm.rep_thm thm in
+    add_term_tvarnames (prop, used)
+    |> fold (curry add_term_tvarnames) hyps
+    |> fold (curry add_term_tvarnames) (Thm.terms_of_tpairs tpairs)
+  end;
+
 
 
 (** basic attributes **)
@@ -681,7 +690,7 @@
 (*Use a conversion to transform a theorem*)
 fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
 
-(*** SOME useful meta-theorems ***)
+(*** Some useful meta-theorems ***)
 
 (*The rule V/V, obtains assumption solving for eresolve_tac*)
 val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "PROP ?psi"));
@@ -813,7 +822,7 @@
 
 fun read_instantiate_sg sg sinsts th =
     let val ts = types_sorts th;
-        val used = add_term_tvarnames (prop_of th, []);
+        val used = add_used th [];
         val sinsts' = map (apfst Syntax.indexname) sinsts
     in  instantiate (read_insts sg ts ts used sinsts') th  end;