src/Pure/drule.ML

   val read_instantiate	: (string*string)list -> thm -> thm
   val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
   val read_insts	:
           Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
                   -> (indexname -> typ option) * (indexname -> sort option)
-                  -> (string*string)list
+                  -> string list -> (string*string)list
                   -> (indexname*ctyp)list * (cterm*cterm)list
   val reflexive_thm	: thm
   val revcut_rl		: thm
   val rewrite_goal_rule	: bool*bool -> (meta_simpset -> thm -> thm option)
         -> meta_simpset -> int -> thm -> thm

   error("No such variable in term: " ^ Syntax.string_of_vname ixn);
 
 fun inst_failure ixn =
   error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
 
-fun read_insts sign (rtypes,rsorts) (types,sorts) insts =
+fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
 let val {tsig,...} = Sign.rep_sg sign
     fun split([],tvs,vs) = (tvs,vs)
       | split((sv,st)::l,tvs,vs) = (case explode sv of
                   "'"::cs => split(l,(indexname cs,st)::tvs,vs)
                 | cs => split(l,tvs,(indexname cs,st)::vs));

             val T = Sign.read_typ (sign,sorts) st;
         in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
            else inst_failure ixn
         end
     val tye = map readT tvs;
-    fun add_cterm ((cts,tye), (ixn,st)) =
+    fun add_cterm ((cts,tye,used), (ixn,st)) =
         let val T = case rtypes ixn of
                       Some T => typ_subst_TVars tye T
                     | None => absent ixn;
-            val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);
+            val (ct,tye2) = read_def_cterm(sign,types,sorts) used false (st,T);
             val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
-        in ((cv,ct)::cts,tye2 @ tye) end
-    val (cterms,tye') = foldl add_cterm (([],tye), vs);
+            val used' = add_term_tvarnames(term_of ct,used);
+        in ((cv,ct)::cts,tye2 @ tye,used') end
+    val (cterms,tye',_) = foldl add_cterm (([],tye,used), vs);
 in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
 
 
 
 (*** Printing of theories, theorems, etc. ***)

       | _ =>   raise THM("COMP", 1, [tha,thb]);
 
 (*Instantiate theorem th, reading instantiations under signature sg*)
 fun read_instantiate_sg sg sinsts th =
     let val ts = types_sorts th;
-    in  instantiate (read_insts sg ts ts sinsts) th  end;
+    in  instantiate (read_insts sg ts ts [] sinsts) th  end;
 
 (*Instantiate theorem th, reading instantiations under theory of th*)
 fun read_instantiate sinsts th =
     read_instantiate_sg (#sign (rep_thm th)) sinsts th;