diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/Argo/argo_tactic.ML
--- a/src/HOL/Tools/Argo/argo_tactic.ML	Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/Argo/argo_tactic.ML	Tue Apr 18 22:24:48 2023 +0200
@@ -656,7 +656,7 @@
 
 (* normalizing goals *)
 
-fun instantiate v ct = Thm.instantiate (TVars.empty, Vars.make [(v, ct)])
+fun instantiate v ct = Thm.instantiate (TVars.empty, Vars.make1 (v, ct))
 
 fun instantiate_elim_rule thm =
   let