--- a/src/HOL/Tools/SMT/smt_util.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_util.ML Fri Sep 10 14:59:19 2021 +0200
@@ -173,7 +173,8 @@
let val cpat = Thm.global_cterm_of thy (Const (name, Sign.the_const_type thy name))
in (destT (Thm.ctyp_of_cterm cpat), cpat) end
-fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (map (dest_TVar o Thm.typ_of) cTs ~~ cUs, []) ct
+fun instTs cUs (cTs, ct) =
+ Thm.instantiate_cterm (TVars.make (map (dest_TVar o Thm.typ_of) cTs ~~ cUs), Vars.empty) ct
fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
fun instT' ct = instT (Thm.ctyp_of_cterm ct)