diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/SMT/smt_util.ML
--- 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)