diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Sep 10 14:59:19 2021 +0200
@@ -943,7 +943,7 @@
      end
 
     fun instantiate_tac from to =
-      PRIMITIVE (Thm.instantiate ([], [(from, to)]))
+      PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make [(from, to)]))
 
     val tactic =
       if is_none var_opt then no_tac