--- 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';