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.

Latest version of METIS_TAC.

The biggest change is that scheduling provers is done by number of
inferences, not time used, so METIS_TAC is now completely
deterministic. If it works for you on a subgoal, it will work every
time HOL4 is built.

New version of Metis:

+ Uses finite models to guide clause selection in resolution.
+ A Metis test for when HOL is compiled using MLton.