diff -r 35a1788dd6f9 -r dd222e2af01a src/Pure/ex/Guess.thy
--- a/src/Pure/ex/Guess.thy	Tue Apr 18 21:47:40 2023 +0200
+++ b/src/Pure/ex/Guess.thy	Tue Apr 18 22:24:48 2023 +0200
@@ -174,7 +174,7 @@
       [] [] [(Binding.empty_atts, [(Logic.mk_term goal, []), (goal, [])])]
     |> snd
     |> Proof.refine_singleton (Method.Basic (fn _ => fn _ => CONTEXT_TACTIC
-        (PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make [(guess, Thm.cterm_of ctxt thesis)]))
+        (PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make1 (guess, Thm.cterm_of ctxt thesis)))
           THEN Goal.conjunction_tac 1
           THEN resolve_tac ctxt [Drule.termI] 1)))
   end;