Change AncestryData API a little

- In particular, make it clear that we expect lists of deltas that are
then applied to values to update them (with a foldl)
- Also hint at next step with (commented out) fullmake entry-point.

Make more visible in the GrammarDeltas signature

Make grammar-deltas s-expressions when stored in theory .dat files

This makes them more legible, and is also a prelude to being more
uniform in the treatment of theory data that merges deltas across
ancestors.

Allow users' theory data to share/hash embedded strings

Make stored theory data HOLsexp's rather than strings

It's easy enough to cope with old code because strings can be injected
into sexps trivially. The richer ThyDataSexp type has been updated to
use a nicer encoder though, and clients that use that API are unchanged.

Be more careful over handling of ThmSetData and rebinding of thm names

In particular, it was previously possible to do

val thm = store_thm("thm[some_attribute]", tm1, tac2);
val thm = store_thm("thm", tm2, tac2);

and have the second thm be exported but to pick up the attribute from
the first call. This is clearly outrageous, so now the attribute is
lost when the second theorem is slotted into the theory.

Working through all this found three places where this
double-definition pattern was happening (there may yet be more). In
src/finite_map and src/list the second theorem was clearly just
redundant and could be deleted.

The example in fun-op-sem is slightly more interesting: there it
defines a function (which definition gives that function a "compute"
attribute), and then restates the definition, saving it under the same
name ("foo_def"). Though arguably bad style, it's important that the
second theorem replace the first, and that it should have the
"compute" attribute. Here the change is to explicitly add that
attribute to the second theorem.

Finally, all this work revealed that Theory.sml's handling of the
NewBinding theory-delta hook was wrong and caused changes to be
dropped after the hook function was called. Debugging *that* led me to
add a pp field to the LoadableThyData registration process so that
theory-data values could be inspected more easily. There is also a
trace variable to turn on some debugging output in Theory.

Clean up handling of type_grammar deltas and interaction with Thyops

Need a slightly better interface for querying the kernel name
signature information for types, and also alter term functions to not
return constants that don't have up-to-date types.

Now deleting a type doesn't result in broken theories.

With a regression test.

Closes #179

Implement "input only type abbreviations"

Closes #599

Preserve add_user_printer properly in grammar data

This requires a slightly involved process for storing references to
code in theory files.

Update the .doc file on add_user_printer (which was already incredibly
long), and add a test.

Closes #367

Handle clear_overloads_on with user-deltas

Convert type-grammars to use deltas for updates

This is very much analogous to what has been done for term grammars.

Add deltas for moving overload operations

Sadly, making an inferior overload is not *quite* the same as making a
normal one, then then moving it "to the back", so I've left both
operations in the user_delta type for the moment.

Handle gen_remove_ovl_mapping

This gets tests as far as string_numTheory

Begin process to use GrammarDeltas inside theories

This doesn't work yet (just attempting to load boolTheory leads to an
exception), but it's close to working, at least for some situations. I'm
generating new constructors for the user_delta type more or less as the
errors prompt me to.

The new constructors in this commit are IOVERLOAD_ON for "add inferior
overload on" (it's not really clear that this is used enough to warrant
inclusion, but hey); ASSOC_RESTR for "associate restriction", which is
used in boolTheory and probably nowhere else ever, and RMOVMAP for
"remove overload mapping", which is used to remove overloadings to
constants.

General pattern in Parse is to generate the user_delta values, and to
then feed these to the term_grammar.add_delta function to make the
grammar updates. This makes Parse simpler on the whole, which is
definitely an improvement.

Record overload_on calls in GrammarDeltas

Record grammar deltas in Parse

These are not used for any other purpose just yet, and the set of
possible grammar deltas is not yet big enough. (Next addition:
overload_on).