src/HOL/Import/import_rule.ML

 fun freezeT thy thm =
   let
     val tvars = Term.add_tvars (Thm.prop_of thm) []
     val tfrees = map (fn ((t, _), s) => TFree (t, s)) tvars
   in
-    Thm.instantiate ((tvars ~~ map (Thm.global_ctyp_of thy) tfrees), []) thm
+    Thm.instantiate (TVars.make (tvars ~~ map (Thm.global_ctyp_of thy) tfrees), Vars.empty) thm
   end
 
 fun def' constname rhs thy =
   let
     val rhs = Thm.term_of rhs

         (case try (assoc (TFree bef)) lambda of
           SOME cty => (iS, cty)
         | NONE => (iS, Thm.global_ctyp_of thy (TFree bef))))
       tys_before tys_after
   in
-    Thm.instantiate (tyinst,[]) th1
+    Thm.instantiate (TVars.make tyinst, Vars.empty) th1
   end
 
 fun inst sigma th =
   let
     val (dom, rng) = ListPair.unzip (rev sigma)

     val thm = Drule.export_without_context_open thm
     val tvs = Term.add_tvars (Thm.prop_of thm) []
     val tns = map (fn (_, _) => "'") tvs
     val nms = fst (fold_map Name.variant tns (Variable.names_of ctxt))
     val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs))
-    val thm' = Thm.instantiate ((tvs ~~ map (Thm.ctyp_of ctxt) vs), []) thm
+    val thm' = Thm.instantiate (TVars.make (tvs ~~ map (Thm.ctyp_of ctxt) vs), Vars.empty) thm
   in
     snd (Global_Theory.add_thm ((binding, thm'), []) thy)
   end
 
 fun log_timestamp () =