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.