src/HOL/Tools/SMT/smt_normalize.ML

 local
   val (cpfalse, cfalse) = `SMT_Util.mk_cprop (Thm.cterm_of \<^context> \<^const>\<open>False\<close>)
 
   fun inst f ct thm =
     let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
-    in Thm.instantiate ([], [(dest_Var (Thm.term_of cv), ct)]) thm end
+    in Thm.instantiate (TVars.empty, Vars.make [(dest_Var (Thm.term_of cv), ct)]) thm end
 in
 
 fun instantiate_elim thm =
   (case Thm.concl_of thm of
     \<^const>\<open>Trueprop\<close> $ Var (_, \<^typ>\<open>bool\<close>) => inst Thm.dest_arg cfalse thm

   fun insert_trigger_conv [] ct = Conv.all_conv ct
     | insert_trigger_conv ctss ct =
         let
           val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct
           val inst = map (apfst (dest_Var o Thm.term_of)) [cp, (ctr, mk_trigger ctss)]
-        in Thm.instantiate ([], inst) trigger_eq end
+        in Thm.instantiate (TVars.empty, Vars.make inst) trigger_eq end
 
   fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct =
     let
       val (lhs, rhs) = dest_cond_eq ct
 

 
 fun add_int_of_nat_constraints thms =
   let val (q, cts) = fold (add_apps add_int_of_nat [] o Thm.cprop_of) thms (false, [])
   in
     if q then (thms, nat_int_thms)
-    else (thms, map (fn ct => Thm.instantiate ([], [(var, ct)]) int_thm) cts)
+    else (thms, map (fn ct => Thm.instantiate (TVars.empty, Vars.make [(var, ct)]) int_thm) cts)
   end
 
 val setup_nat_as_int =
   SMT_Builtin.add_builtin_typ_ext (\<^typ>\<open>nat\<close>,
     fn ctxt => K (Config.get ctxt SMT_Config.nat_as_int)) #>