src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML

     val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)
     val (pats', _, ctxt3) = fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
     fun rewrite_pat (ct1, ct2) =
       (ct1, Thm.cterm_of ctxt3 (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2)))
     val t_insts' = map rewrite_pat (Vars.dest t_insts)
-    val intro'' = Thm.instantiate (TVars.dest T_insts, t_insts') intro
+    val intro'' = Thm.instantiate (T_insts, Vars.make t_insts') intro
     val [intro'''] = Variable.export ctxt3 ctxt [intro'']
     val intro'''' =
       Simplifier.full_simplify
         (put_simpset HOL_basic_ss ctxt
           addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm prod.inject}])

     val U = TFree ("'u", \<^sort>\<open>type\<close>)
     val y = Free (yname, U)
     val f' = absdummy (U --> T') (Bound 0 $ y)
     val th' =
       Thm.instantiate
-        ([(dest_TVar uninst_T, Thm.ctyp_of ctxt' (U --> T')),
+        (TVars.make [(dest_TVar uninst_T, Thm.ctyp_of ctxt' (U --> T')),
           (dest_TVar uninst_T', Thm.ctyp_of ctxt' T')],
-         [((fst (dest_Var f), (U --> T') --> T'), Thm.cterm_of ctxt' f')]) th
+         Vars.make [((fst (dest_Var f), (U --> T') --> T'), Thm.cterm_of ctxt' f')]) th
     val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th']
   in
     th'
   end
 

                 raise Fail "Trying to instantiate another predicate"
               else ()
             val instT =
               TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T))
                 (subst_of (pred', pred)) [];
-          in Thm.instantiate (instT, []) th end
+          in Thm.instantiate (TVars.make instT, Vars.empty) th end
         fun instantiate_ho_args th =
           let
             val (_, args') =
               (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) th
             val ho_args' = map dest_Var (ho_args_of_typ T args')
-          in Thm.instantiate ([], ho_args' ~~ map (Thm.cterm_of ctxt') ho_args) th end
+          in
+            Thm.instantiate (TVars.empty, Vars.make (ho_args' ~~ map (Thm.cterm_of ctxt') ho_args))
+              th
+          end
         val outp_pred =
           Term_Subst.instantiate (subst_of (inp_pred, pred), Vars.empty) inp_pred
         val ((_, ths'), ctxt1) =
           Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
       in