src/HOL/Tools/Lifting/lifting_setup.ML

     val param_rel_subst = Envir.subst_term (tyenv_match,Vartab.empty) param_rel
     val args_subst = map (Envir.subst_term (tyenv_match,Vartab.empty)) args
     val (instT, lthy2) = lthy1
       |> Variable.declare_names fixed_crel
       |> Variable.importT_inst (param_rel_subst :: args_subst)
-    val args_fixed = (map (Term_Subst.instantiate (instT, []))) args_subst
-    val param_rel_fixed = Term_Subst.instantiate (instT, []) param_rel_subst
+    val args_fixed = (map (Term_Subst.instantiate (instT, Term_Subst.Vars.empty))) args_subst
+    val param_rel_fixed = Term_Subst.instantiate (instT, Term_Subst.Vars.empty) param_rel_subst
     val rty = (domain_type o fastype_of) param_rel_fixed
     val relcomp_op = Const (\<^const_name>\<open>relcompp\<close>, 
           (rty --> rty' --> HOLogic.boolT) --> 
           (rty' --> qty --> HOLogic.boolT) --> 
           rty --> qty --> HOLogic.boolT)

 local
   fun importT_inst_exclude exclude ts ctxt =
     let
       val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []))
       val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt
-    in (tvars ~~ map TFree tfrees, ctxt') end
+    in (Term_Subst.TVars.table (tvars ~~ map TFree tfrees), ctxt') end
   
   fun import_inst_exclude exclude ts ctxt =
     let
       val excludeT = fold (Term.add_tvarsT o snd) exclude []
       val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt
       val vars = map (apsnd (Term_Subst.instantiateT instT)) 
         (rev (subtract op= exclude (fold Term.add_vars ts [])))
       val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt'
-      val inst = vars ~~ map Free (xs ~~ map #2 vars)
+      val inst = Term_Subst.Vars.table (vars ~~ map Free (xs ~~ map #2 vars))
     in ((instT, inst), ctxt'') end
   
   fun import_terms_exclude exclude ts ctxt =
     let val (inst, ctxt') = import_inst_exclude exclude ts ctxt
     in (map (Term_Subst.instantiate inst) ts, ctxt') end