Remove Globals.priming.

Also remove references to it in code that isn't being tested in the
regression checking build-sequence, and so is probably bit-rotted.

Provide numvariant version of variant, which behaves like

with_flag(Globals.priming,SOME "") (variant avoids)

Document change/incompatibility in release notes.

Move lambda type, dest_term function to kernel; add identical fn

dest_term is quite heavily used (it implements SML's best
approximation of a "view" for pattern-matching against terms), and its
implementation outside the kernel is needlessly inefficient.

Also extend signature with identical function, which correctly says
whether or not two terms are identical, including in their choice of
bound names. In the standard kernel, the possible presence of
explicit substitution terms means that this notion is not the same as
simple equality on terms.

Remove eqtype declaration for term type

Put equality constant into signature for Term

Put a fast/approximate equality check into Term API

This points at the pointer-equality function for the moment, but
should eventually be swung to point at something that works reliably
and doesn't cause strange unreproducible crashes.

Extend kernel API with new all_atoms entrypoint.

Use this in theory pretty-printing routine to deal with issue #115.

Closes #115.

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.)

Handle the discrepancy in the behaviour between the way CHOOSE_THEN
and GEN_TAC choose variants by making them do the same thing (Konrad
earlier fixed GEN_TAC to use prim_variant, but CHOOSE_THEN was using
variant).

Decided that avoiding constant names in the current grammar was
probably a good idea, so open up the internal gen_variant function in
Term.sml, and feed it with the new predicate "is_constname" from
Parse. is_constname is true if a string is the name of a "constant"
as the parser sees things. In particular, if you do
overload_on ("foo", ``SUC``)
then "foo" (as well as "SUC") will be considered a const's name.

Hidden constants are not const names in this sense, so C doesn't get
primed in either of
STRIP_TAC ([], ``(?C. P C) ==> Q``)
or
STRIP_TAC ([], ``!C. P C ==> Q``)
even with combinTheory as an ancestor.

Size functions for terms and types that count the size of the
respective trees. Have written these so many times that it seems
useful to have them in the kernel and available for all. (The
term_size function doesn't include the sizes of the attached types;
haven't ever felt the need for this.)

Rework a bunch of code in the two kernels so that they can share even
more stuff in src/prekernel. In particular, the latter is now home to
a special purpose symbol table that knows all about things being
up-to-date. Also move the final signatures for Terms and Types that
are what is ultimately presented to the user into prekernel so that
both kernels can use them.
In src/0 also move the signatures in Raw-sig into Type.sig and
Term.sig so that {Type,Term}.sml can be compiled in normal mode
against those signatures. I think this makes things a deal cleaner
there.
Finally, witnesses have entirely disappeared from src/0. If we
wanted to reinstate them for whatever reason, they could be stored in
a KernelSig.symbol_table along with arities and base types.