src/Pure/Isar/subgoal.ML

     val Ts = map Thm.typ_of_cterm params;
     val ts = map Thm.term_of params;
 
     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 =
       let
         val ((x, i), T) = v;