Throw more exceptions when SharingTables lookups go wrong

Use "string-hashing" for theory names occuring in thm dep info

Use string table to "hash" theorem names in main theorem list

Complete refactoring of Sharing code

There's now an API for exporting theorems, terms and types to
s-expressions that should be generally useful (not just in the theory
data management setting).

Start to refactor Sharing code

Fix SharingTables.sml to compile under Moscow ML

Delete some unused code

Change theory files to use an s-expression representation

This wastes some disk-space in the form of extra white-space that the
Oppen pretty-printer introduces for indentation purposes, but with the
string table used, the number of lines and the number of
non-whitespace characters is lower.

The string table can and will be used in more places in subsequent
commits to try to improve file size and sharing. The theory data may
also shift to directly use s-expressions rather than strings (people
wedded to a string representation can always embed those into
s-expressions of course).

Optimise theory dat space a bit

- use a slightly more compact term representation that saves a bit of
space when binary or unary applications happen
- build a table of strings to reuse at the top of theory files

The strings table still needs to be used in a bunch more places
throughout Theory.dat files.

Move smpp to Portable - get everything up to arithmeticScript working

Work towards use of PolyML.pretty type for most pretty-printing

Compiles up to src/parse under Poly/ML

Use _Theory.dat for loading theory data into _Theory.sml

BIG refactor: mainly to allow stdknl to use SharingTables technology.

SharingTables implements hash-consing for types as they are written
out to disk. This can make a big difference to the theory file size,
and thus to theory-loading times.

The big visible change is that Theory, TheoryPP and Definition are no
longer really part of the kernel, and are found in src/postkernel
instead. They don't need to know about secret implementation details
in terms, types or theorems. They do need to have access to

Term.{write,read}_raw

and primitive definition principles (which are in Thm).

Another API change is that Tags no longer use user-visible string refs
to record use of axioms. Instead, the refs are hidden behind a new
Nonce type. This in turn means that the Tag.axioms_of function can
move to be visible to all users after the kernel. (If we kept the
axioms as string refs, users could alter the strings being pointed
to.)