Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

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.

Change to structure of numLib so that reduce and arith are incorporated.