replace add_persistent_funs with a LoadableThyData version

Progress on #73. Haven't touched the "del" variant yet: ThmSetData has
less support for deleting at the moment, and not sure what is actually
necessary.
make Defn.add_persistent_funs play nice with new compLib version (#73)

compLib.add_persistent_funs previously accepted a string that was
arbitrary code to be printed at the end of a theory. Now it must be the
name of a theorem in the current theory.

Defn was running SUC_TO_NUMERAL_DEFN_CONV in the printed code; now it
saves a theorem with the result of the conversion and uses its name
instead.
make patricia play nice with new add_persistent_funs (#73)

Some theories in src/patricia were calling add_persistent_funs for
definitions from other theories (list and pred_set) and using the
arbitrary code string to refer to those theorems with fully qualified
names.

The fix adopted here is to call add_persistent_funs for those constants
in the theories where they are defined.
change interface to add_persistent_funs (#73) and fix more calls

The new interface takes a list of strings naming theorems.
(The old interface took a list of (string * thm) pairs.)
The new way better ensures consistency of theory development and theory
load behaviour: you can no longer pass a name with a theorem that isn't
actually saved under it.

Theorems are looked up with DB.theorem, or failing that, DB.definition
or DB.axiom.

Alas, I found more examples using add_persistent_funs to add theorems in
ancestor theories. Rather than modify the ancestor theories, I have
opted to make the offending theories save the theorems they want to add
to computeLib themselves so they have a name in the current theory to
pass to add_persistent_funs.

If this behavior was appropriate for patricia too (da47401) change it.
Alternatively, if the ancestor theories should have exported those
things for computeLib anyway, search this commit for new instances of
"save_thm" to see what needs fixing.
Delete some unused code in ThmSetData.sml
Make theorem-set loading more robust in face of bad thm-names.

Most attempts to mess with the data will be caught at specification
time, but use of delete_const and friends can cause theorems to not
get exported even if they were present when the call to export_X was
made.
Revert "make patricia play nice..."

This reverts commit da47401d5163b28a320790e7acca897d8374880c.
Reason: qualified names in the list of add_persistent_funs exports are
supposed to work.
See comments on #73.
The reason why they probably weren't working before is that you need to
use a name like:
  "pred_set.FINITE_EMPTY"
not
  "pred_setTheory.FINITE_EMPTY"

Conflicts:
	src/list/src/listScript.sml
	src/patricia/patriciaScript.sml
	src/patricia/patricia_castsScript.sml
	src/pred_set/src/pred_setScript.sml

(Conflicts all due to change in add_persistent_funs interface.)
revert some of 0fc7587: allow add_persistent_funs of other consts
make add_persistent_funs use ThmSetData's export properly (#73)

the returned export function calls the addfn function itself, so there's
no need to do that manually.
Rework various Theory hooks into one general framework.

The basis for the framework is the TheoryDelta type. Client code can
ask to be notified of theory changes, and will have their provided
call-back function called at appropriate times.

This commit hasn't adjusted the theory functions for
{add,del}{const/typeOp} yet; it has just unified the existing
functionality (register_onload, after_new_theory and
register_onexport).
More theory signature events now reported to hooks.

In particular, {new,remove}{typeOp,constant} events are reported.

Use this to do away with some of the cruftiness in boolLib whereby the
entry-points there had to mask the primitive principles in order to
update the grammar. Now the parser installs hooks to watch for things
being deleted or added and adjusts the grammar as it goes.

The disadvantage is that it's impossible to bypass these changes to
the grammar.
Give better error when client tries to reuse a theory data key
Provide lookup functionality across all stored theorem sets.
Merge branch 'master' into persistent_funs
Merge branch 'master' into persistent_funs
Allow thy-data to be set to a value as well as merged with what's there.
Minor code cleanup in Theory.sml's handling of theory data.
Get stored ThmSets to notice deletion of relevant consts.

This is progress with #73.
Adjust (and reduce) interface to ThmSetData.

The change is to add an extra string parameter to the callback
function that the client provides. This is the name of the theory
which has stored the theorems. This change prompted the changes to
computeLib, IndDefLib and DefnBase.

The reduction was to remove the ThmSetData's new function, forcing
BasicProvers to use new_exporter. This was possible because of the
extra information provided to its call-back.

I also wrote some test-cases mimicking the original problem that
Magnus and Ramana had, and prettied the warning output.

This closes #73.