--- a/src/Pure/type_infer.ML Thu Sep 09 23:05:33 2021 +0200
+++ b/src/Pure/type_infer.ML Thu Sep 09 23:07:02 2021 +0200
@@ -116,8 +116,9 @@
val used' = Name.declare a used;
in (TVars.add ((xi, S), TFree (a, improve_sort S)) inst, used') end
else (inst, used);
+ val params = TVars.build (fold TVars.add_tvars ts) |> TVars.list_set;
val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
- val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) (TVars.empty, used);
+ val (inst, _) = fold subst_param params (TVars.empty, used);
in (map o map_types) (Term_Subst.instantiateT inst) ts end;
end;