src/Pure/Isar/subgoal.ML

--- a/src/Pure/Isar/subgoal.ML	Thu Sep 09 23:05:33 2021 +0200
+++ b/src/Pure/Isar/subgoal.ML	Thu Sep 09 23:07:02 2021 +0200
@@ -89,7 +89,7 @@
 
     val prop = Thm.full_prop_of th';
     val concl_vars = Vars.build (Vars.add_vars (Logic.strip_imp_concl prop));
-    val vars = build_rev (Term.add_vars prop);
+    val vars = Vars.build (Vars.add_vars prop) |> Vars.list_set;
     val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
 
     fun var_inst v y =