--- 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