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.

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

Fixes an error in METIS_TAC for boundary cases of genvars.

The arity function in mlibTermorder.sml made use of String.compare
to compare two strings, including the names of genvars.

The problem with this is that while

> String.compare ("%%genvar%%999","%%genvar%%998");
val it = GREATER : order

sometimes we have

> String.compare ("%%genvar%%1000","%%genvar%%999");
val it = LESS : order

This is important, and has led to METIS_TAC failing when it would have
worked if the genvar numbers had been one less or one more.

Joe Hurd, the author of METIS_TAC, has been informed and has agreed
with this change:

"Thank you for such a detailed bug report together with a thoughtful
analysis of the underlying problem and a suggested patch. I completely
agree with your reasoning, and I think your patch will help to make
METIS_TAC more deterministic (an important consideration for an
interactive theorem prover).

Please commit your patch with my blessing."

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!

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 with a more powerful prover engine.

Another bugfix: this time to the Metis implementation of term orderings.

Fixed a bug discovered by Konrad, where the new version of metis couldn't
prove something the previous version could.

Version 1.3: 17 June 2002

Goals submitted to MESON_TAC when HOL is built .......... 1953
Proved by MESON_TAC ..................................... 1953
Proved by METIS_TAC within 10s .......................... 1946

Between Versions 1.2 and 1.3

* Implemention of definitional CNF to reduce blow-up in number of
clauses (usually caused by nested boolean equivalences).
* Resolution is more robust and efficient, and includes an option
(off by default) for clauses to inherit ordering constraints.