diff -r 633fe7390c97 -r 612b7e0d6721 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -45,7 +45,7 @@
      ('a -> thm -> 'b Seq.seq) -> 'a -> thm -> 'b Seq.seq
   val try_dest_Trueprop : term -> term
 
-  val type_devar : typ Term_Subst.TVars.table -> term -> term
+  val type_devar : typ TVars.table -> term -> term
   val diff_and_instantiate : Proof.context -> thm -> term -> term -> thm
 
   val batter_tac : Proof.context -> int -> tactic
@@ -573,7 +573,7 @@
     val typeval = map (fn (v, T) => (dest_TVar v, Thm.ctyp_of ctxt T)) type_pairing
 
     val typeval_env =
-      Term_Subst.TVars.table (map (apfst dest_TVar) type_pairing)
+      TVars.make (map (apfst dest_TVar) type_pairing)
     (*valuation of term variables*)
     val termval =
       map (apfst (dest_Var o type_devar typeval_env)) term_pairing