diff -r b3c65c984210 -r 1091880266e5 src/Pure/Isar/subgoal.ML
--- a/src/Pure/Isar/subgoal.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/Isar/subgoal.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -88,7 +88,7 @@
     val ts = map Thm.term_of params;
 
     val prop = Thm.full_prop_of th';
-    val concl_vars = Term_Subst.add_vars (Logic.strip_imp_concl prop) Term_Subst.Vars.empty;
+    val concl_vars = Term_Subst.Vars.build (Term_Subst.add_vars (Logic.strip_imp_concl prop));
     val vars = rev (Term.add_vars prop []);
     val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';