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

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

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

A better fix for the bug found by Scott Owen.

Fix for a bug found by Scott Owen.

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.

Fixed a bug found by Michael Norrish whereby definitional CNF interacted
badly with type reconstruction. This resulted in some invocations of
METIS_TAC returning "error during proof translation", and then failing to
find a proof with types switched on. All fixed now.

Now that STRIP_TAC has changed, METIS_TAC can safely do pre-normalization
splitting using DISJ_CASES_THEN. The only user-visible result of this
should be better performance.

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.

Version 1.2: 19 November 2002

Goals submitted to MESON_TAC when HOL is built .......... 1779
Proved by MESON_TAC ..................................... 1779
Proved by METIS_TAC within 10s .......................... 1774

Between Versions 1.1 and 1.2

* Ground-up reimplementation of the resolution calculus, which now
performs ordered resolution and ordered paramodulation.
* A single entry-point METIS_TAC, which uses heuristics to decide
whether to apply FO_METIS_TAC or HO_METIS_TAC.
* {HO|FO}_METIS_TAC both initially operate in typeless mode, and
automatically try again with types if an error occurs during proof
translation.
* Extensionality axiom now included in HO_METIS_TAC by default.