Ensure HOL4 works with fixed-width integers under Poly/ML.

Integers under Poly/ML 5.6.1 are likely to be fixed-width by default (up until now they've always been arbitrary precision). Some changes were needed to cope with this:

- The Arbint and Artbnum structures effectively assumed Int.int = IntInf.int.
- The Standard ML structure Time is based on LargeInt.int and not Int.int. Code for printing times has been re-implemented using the Date structure.
- The smart-configure.sml file used the Overflow exception to distinguish between Moscow ML and Poly/ML. This test is now based on a difference in the printing of General.Fail exceptions.

More assorted code tidying.

Remove trailing whitespace in source files.

Fixed the toString function to suffix an "i" again, just like it does
under Moscow ML. (The behavior under Poly/ML was different since r7578.)

Perhaps one should instead get rid of the "i" (under both Poly/ML and
Moscow ML). For instance, fromString o toString is currently not working
as one might expect.

The PolyML version now uses PolyML's builin IntInf support. (This change
doesn't appear to speed up HOL, but it's nice to have anyway.)