--- a/src/Pure/type_infer.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/type_infer.ML Thu Sep 09 12:33:14 2021 +0200
@@ -114,10 +114,10 @@
let
val [a] = Name.invent used Name.aT 1;
val used' = Name.declare a used;
- in (Term_Subst.TVars.add ((xi, S), TFree (a, improve_sort S)) inst, used') end
+ in (TVars.add ((xi, S), TFree (a, improve_sort S)) inst, used') end
else (inst, used);
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 []) (Term_Subst.TVars.empty, used);
+ val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) (TVars.empty, used);
in (map o map_types) (Term_Subst.instantiateT inst) ts end;
end;