The traditional ML datatype term is rather redundant concerning the type of Const items: the full type-instance is provided. This simplifies a function like Term.type_of, but is rather costly for type instantiation (e.g. Thm.instantiate and many related operations). An alternative is to store only the typargs in Const, and use the underlying type signature reconstruct the full type instance where this is actually required (see also Consts.typargs, Consts.instance). There could be a new function Consts.type_of to check/compute the type of a term without creating full type instances first.

For example, instances of a constant declared as op :: "'a ⇒ 'a ⇒ 'a" occurr in the old scheme as Const ("A.op", "T ⇒ T ⇒ T") with duplications of the potentially large substructure T and redundant outline for the whole type; the new scheme would only have Const ("A.op", [T]) and type instantiation/unification/matching only needs to take the single T into account.

This is a substantial reform of low-level term representation: it could impact the performance of the inference kernel significantly, because polymorphic constants with large type-schemes are ubiquitious in applications. It is probably also a lot of work to implement, and special use of non-logical terms (e.g. in syntax asts and translations) needs to be adapted.