src/Pure/drule.ML
changeset 15669 2b1f1902505d
parent 15574 b1d1b5bfc464
child 15797 a63605582573
     1.1 --- a/src/Pure/drule.ML	Thu Apr 07 09:27:09 2005 +0200
     1.2 +++ b/src/Pure/drule.ML	Thu Apr 07 09:27:20 2005 +0200
     1.3 @@ -86,6 +86,7 @@
     1.4    include BASIC_DRULE
     1.5    val strip_comb: cterm -> cterm * cterm list
     1.6    val strip_type: ctyp -> ctyp list * ctyp
     1.7 +  val add_used: thm -> string list -> string list
     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 @@ -252,8 +253,9 @@
    1.12  ***)
    1.13  
    1.14  fun types_sorts thm =
    1.15 -    let val {prop,hyps,...} = rep_thm thm;
    1.16 -        val big = list_comb(prop,hyps); (* bogus term! *)
    1.17 +    let val {prop, hyps, tpairs, ...} = Thm.rep_thm thm;
    1.18 +        (* bogus term! *)
    1.19 +        val big = list_comb (list_comb (prop, hyps), Thm.terms_of_tpairs tpairs);
    1.20          val vars = map dest_Var (term_vars big);
    1.21          val frees = map dest_Free (term_frees big);
    1.22          val tvars = term_tvars big;
    1.23 @@ -262,6 +264,13 @@
    1.24          fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i));
    1.25      in (typ,sort) end;
    1.26  
    1.27 +fun add_used thm used =
    1.28 +  let val {prop, hyps, tpairs, ...} = Thm.rep_thm thm in
    1.29 +    add_term_tvarnames (prop, used)
    1.30 +    |> fold (curry add_term_tvarnames) hyps
    1.31 +    |> fold (curry add_term_tvarnames) (Thm.terms_of_tpairs tpairs)
    1.32 +  end;
    1.33 +
    1.34  
    1.35  
    1.36  (** basic attributes **)
    1.37 @@ -681,7 +690,7 @@
    1.38  (*Use a conversion to transform a theorem*)
    1.39  fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
    1.40  
    1.41 -(*** SOME useful meta-theorems ***)
    1.42 +(*** Some useful meta-theorems ***)
    1.43  
    1.44  (*The rule V/V, obtains assumption solving for eresolve_tac*)
    1.45  val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "PROP ?psi"));
    1.46 @@ -813,7 +822,7 @@
    1.47  
    1.48  fun read_instantiate_sg sg sinsts th =
    1.49      let val ts = types_sorts th;
    1.50 -        val used = add_term_tvarnames (prop_of th, []);
    1.51 +        val used = add_used th [];
    1.52          val sinsts' = map (apfst Syntax.indexname) sinsts
    1.53      in  instantiate (read_insts sg ts ts used sinsts') th  end;
    1.54