diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Fri Sep 10 14:59:19 2021 +0200
@@ -579,7 +579,7 @@
       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?*)