# HG changeset patch
# User ballarin
# Date 1068816955 -3600
# Node ID a7ef3f7588c5aa79828b6442793098ec980da7c6
# Parent  33e5ef9a4c98b879d8daed40ab9d9055b228c614
Type inference bug in Isar attributes "where" and "of" fixed.

diff -r 33e5ef9a4c98 -r a7ef3f7588c5 NEWS
--- a/NEWS	Wed Nov 12 10:58:23 2003 +0100
+++ b/NEWS	Fri Nov 14 14:35:55 2003 +0100
@@ -41,6 +41,11 @@
     longer be enclosed in quotes.  Instead, precede variable name with `?'.
     This is consistent with the instantiation attribute "where".
 
+* Attributes "where" and "of":
+  Now take type variables of instantiated theorem into account when reading
+  the instantiation string.  This fixes a bug that caused instantiated
+  theorems to have too special types in some circumstances.
+
 * Locales:
   - Goal statements involving the context element "includes" no longer
     generate theorems with internal delta predicates (those ending on
diff -r 33e5ef9a4c98 -r a7ef3f7588c5 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Nov 12 10:58:23 2003 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Nov 14 14:35:55 2003 +0100
@@ -212,7 +212,12 @@
         val (xs, ss) = Library.split_list insts;
         val Ts = map get_typ xs;
 
-        val (ts, envT) = ProofContext.read_termTs ctxt (ss ~~ Ts);
+        val used = add_term_tvarnames (prop_of thm,[])
+        (* Names of TVars occuring in thm.  read_termTs ensures
+           that new TVars introduced when reading the instantiation string
+           are distinct from used ones. *)
+
+        val (ts, envT) = ProofContext.read_termTs used ctxt (ss ~~ Ts);
         val cenvT = map (apsnd (Thm.ctyp_of sign)) envT;
         val cenv =
           map (fn (xi, t) => pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t))
diff -r 33e5ef9a4c98 -r a7ef3f7588c5 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Nov 12 10:58:23 2003 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Nov 14 14:35:55 2003 +0100
@@ -29,7 +29,7 @@
   val cert_typ_no_norm: context -> typ -> typ
   val get_skolem: context -> string -> string
   val extern_skolem: context -> term -> term
-  val read_termTs: context -> (string * typ) list -> term list * (indexname * typ) list
+  val read_termTs: string list -> context -> (string * typ) list -> term list * (indexname * typ) list
   val read_termTs_env: (indexname -> typ option) * (indexname -> sort option) * string list -> context -> (string * typ) list -> term list * (indexname * typ) list
   val read_term: context -> string -> term
   val read_prop: context -> string -> term
@@ -591,8 +591,10 @@
   end
 in
 
-val read_termTs =
-  gen_read (read_def_termTs false) (apfst o map) None false false false false;
+(* For where attribute:
+   Type vars generated by read will be distinct from those in "used". *)
+fun read_termTs used =
+  gen_read (read_def_termTs false) (apfst o map) (Some (K None, K None, used)) false false false false;
 (* For rule_tac:
    takes extra environment (types, sorts and used type vars) *)
 fun read_termTs_env env =