eliminated some ref-matches

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.

Moved a bunch of things from tools-poly/poly to portableML/poly.

Still to do: make Poly Arb{int,num} use Poly's built-in arbitrarily
large integer type. Also want to get rid of the last remaining
"redirect" in tools-poly/poly/poly-init2.ML.