Standard and experimental kernels now share Thm.sml implementation

It should now be possible to have the logging kernel work over either
implementation of terms, and to delete its copy of Type, Term etc.

Trivial cleanup.

Updated documentation for term nets, and made the type of nets abstract.

Massive changes. Most are trivial and due to the shrinking of portableML.
More significantly, type antiquotations are no longer part of the
term representation.

Term nets have also been generally improved, and given a more extensive
interface. Documentation can be found at Net.sig.

Initial revision