src/Pure/Isar/attrib.ML
changeset 14257 a7ef3f7588c5
parent 14082 c69d5bf3047d
child 14287 f630017ed01c
--- 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))