src/HOL/Tools/Argo/argo_tactic.ML

--- a/src/HOL/Tools/Argo/argo_tactic.ML	Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Argo/argo_tactic.ML	Fri Sep 10 14:59:19 2021 +0200
@@ -305,7 +305,8 @@
   let val cprop = as_prop ct
   in Thm.implies_intr cprop (f (Thm.assume cprop)) end
 
-fun instantiate cv ct = Thm.instantiate ([], [(Term.dest_Var (Thm.term_of cv), ct)])
+fun instantiate cv ct =
+  Thm.instantiate (TVars.empty, Vars.make [(Term.dest_Var (Thm.term_of cv), ct)])
 
 
 (* proof replay for tautologies *)