Fudge around strange quirk with timers stored in Poly heaps

*** empty log message ***

Rewrote both kernels to cope with Overflow in Time.toSeconds by instead
going via a real, and using Arbnum. Also simplified the thyid type in
Theory.sml so that the representation was a pair of nums rather than a
time value that was being converted into and out of.

Made a bunch of changes to the HOL source to make it more "Standard ML",
to make it easier to port to MLton.

For example:
+ Added lots of structure wrappers around miscellaneous .sml files.
+ The type of "before" is 'a * () -> 'a, not 'a * 'b -> 'a, as Moscow ML
currently thinks.
+ Added "val _ = " before random declarations.

A plea: if I'm ever going to succeed in porting HOL to MLton, could
people please stop using Polyhash. It's very useful, but there's
nothing like it in MLton (or indeed Standard ML). In theory I'm going
to have to change the (sometimes complicated) code to use Binarymap or
something like it, but in practice I'll only do that when there's
absolutely no other way.

Can use the Global hol_clock for this.

Added time-stamps to simplifier trace output. Am tempted to move
hol_clock to somewhere like Globals to give the whole system a standard
place to look for time elapsed information.

A couple of changes: caches can be examined in a better way than just
printing them, and a new trace "action", lazy text, which will potentially
save time when a trace is not looked at. (The text might print out a term,
say.)

The interface to the various trace functions has changed slightly.

Paired syntax.

Register the trace_level variable with the global register of trace
variables.

Fixed to bring it up to date with Taupo release 0.
(Changes have come across from parse_branch development.)

Initial revision