src/HOL/Tools/SMT/smt_replay.ML

--- a/src/HOL/Tools/SMT/smt_replay.ML	Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_replay.ML	Fri Sep 10 14:59:19 2021 +0200
@@ -96,7 +96,8 @@
 
 fun compose (cvs, f, rule) thm =
   discharge thm
-    (Thm.instantiate ([], map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm)) rule)
+    (Thm.instantiate
+      (TVars.empty, Vars.make (map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm))) rule)
 
 
 (* simpset *)