Type inference bug in Isar attributes "where" and "of" fixed.
authorballarin
Fri Nov 14 14:35:55 2003 +0100 (2003-11-14)
changeset 14257a7ef3f7588c5
parent 14256 33e5ef9a4c98
child 14258 9bd184c007f0
Type inference bug in Isar attributes "where" and "of" fixed.
NEWS
src/Pure/Isar/attrib.ML
src/Pure/Isar/proof_context.ML
     1.1 --- a/NEWS	Wed Nov 12 10:58:23 2003 +0100
     1.2 +++ b/NEWS	Fri Nov 14 14:35:55 2003 +0100
     1.3 @@ -41,6 +41,11 @@
     1.4      longer be enclosed in quotes.  Instead, precede variable name with `?'.
     1.5      This is consistent with the instantiation attribute "where".
     1.6  
     1.7 +* Attributes "where" and "of":
     1.8 +  Now take type variables of instantiated theorem into account when reading
     1.9 +  the instantiation string.  This fixes a bug that caused instantiated
    1.10 +  theorems to have too special types in some circumstances.
    1.11 +
    1.12  * Locales:
    1.13    - Goal statements involving the context element "includes" no longer
    1.14      generate theorems with internal delta predicates (those ending on
     2.1 --- a/src/Pure/Isar/attrib.ML	Wed Nov 12 10:58:23 2003 +0100
     2.2 +++ b/src/Pure/Isar/attrib.ML	Fri Nov 14 14:35:55 2003 +0100
     2.3 @@ -212,7 +212,12 @@
     2.4          val (xs, ss) = Library.split_list insts;
     2.5          val Ts = map get_typ xs;
     2.6  
     2.7 -        val (ts, envT) = ProofContext.read_termTs ctxt (ss ~~ Ts);
     2.8 +        val used = add_term_tvarnames (prop_of thm,[])
     2.9 +        (* Names of TVars occuring in thm.  read_termTs ensures
    2.10 +           that new TVars introduced when reading the instantiation string
    2.11 +           are distinct from used ones. *)
    2.12 +
    2.13 +        val (ts, envT) = ProofContext.read_termTs used ctxt (ss ~~ Ts);
    2.14          val cenvT = map (apsnd (Thm.ctyp_of sign)) envT;
    2.15          val cenv =
    2.16            map (fn (xi, t) => pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t))
     3.1 --- a/src/Pure/Isar/proof_context.ML	Wed Nov 12 10:58:23 2003 +0100
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Nov 14 14:35:55 2003 +0100
     3.3 @@ -29,7 +29,7 @@
     3.4    val cert_typ_no_norm: context -> typ -> typ
     3.5    val get_skolem: context -> string -> string
     3.6    val extern_skolem: context -> term -> term
     3.7 -  val read_termTs: context -> (string * typ) list -> term list * (indexname * typ) list
     3.8 +  val read_termTs: string list -> context -> (string * typ) list -> term list * (indexname * typ) list
     3.9    val read_termTs_env: (indexname -> typ option) * (indexname -> sort option) * string list -> context -> (string * typ) list -> term list * (indexname * typ) list
    3.10    val read_term: context -> string -> term
    3.11    val read_prop: context -> string -> term
    3.12 @@ -591,8 +591,10 @@
    3.13    end
    3.14  in
    3.15  
    3.16 -val read_termTs =
    3.17 -  gen_read (read_def_termTs false) (apfst o map) None false false false false;
    3.18 +(* For where attribute:
    3.19 +   Type vars generated by read will be distinct from those in "used". *)
    3.20 +fun read_termTs used =
    3.21 +  gen_read (read_def_termTs false) (apfst o map) (Some (K None, K None, used)) false false false false;
    3.22  (* For rule_tac:
    3.23     takes extra environment (types, sorts and used type vars) *)
    3.24  fun read_termTs_env env =