src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML

     (*valuation of term variables*)
     val termval =
       map (apfst (dest_Var o type_devar typeval_env)) term_pairing
       |> map (apsnd (Thm.cterm_of ctxt))
   in
-    Thm.instantiate (typeval, termval) scheme_thm
+    Thm.instantiate (TVars.make typeval, Vars.make termval) scheme_thm
   end
 
 (*FIXME this is bad form?*)
 val try_dest_Trueprop = perhaps (try HOLogic.dest_Trueprop)