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.

Removed Lib.gather. Use {Lib,List}.filter instead.

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Instituting paired syntax. Long live paired syntax!

New Kananaskis kernel.

Um ... what has changed here? Must check.

Introduced explicit substitutions in terms,
and the optimized rules for computeLib.
The invariant about free variables under abstraction is disabled.
Instead, dest_abs computes free variables of the body.
Eta-conversion has moved to Term

Added "enumerate" to Lib.sml. Example:

enumerate 0 ["a", "b", "c"] = [(0,"a"), (1,"b"), (2,"c")]

Also, fixed a performance bug in Net. When attempting to look something up
in an empty net, failure should be immediate (but wasn't).

Trivial cleanup.

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.

"Globals" changed to get rid of outdated variables.
"Theory" changed to make set_MLname be more informative when failing.
NB: similar functions should also be likewise changed.
I'm not sure what the changes to "Net" are: probably trivial syntactic
stuff.

Initial revision