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.