Make minor (semantically no-op) cleanups in src/metis

Label assignments (v := e) as (* OK *) in src/metis

These labels are my judgement that the references are strictly local
and so not a concurrency issue. Additionally, some assignments in
comments (to Moscow ML specific quietdec, for example) have just been
deleted.

Use new Portable.make_counter in various places within src/metis

Isolate assignment to traces ref in metis code

Hide assignment to this reference behind add_trace and set_traces
function calls.

Up to core types

Improvements to Metis made while investigating bad performance reported
by Anthony, Juliano and Mike.

New version of metis: this one actually goes through the compiler
and runs the selftest!

* Implemented a HOL specific finite model, which knows about
numbers, lists and sets.
* Removed multiple provers: METIS_TAC is now solely based on ordered
resolution.

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.