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

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.

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.

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.1 of the Metis Library.

From the Change Log section of the README:

Between Versions 1.0 and 1.1

* Added a "metis" entry to the HOL trace system: it nows prints
status information during proof (if HOL is in interactive mode).
* Restricted (universal and existential) quantifiers are now
normalized by the NNF conversion.
* (First-order) METIS_TAC can now handle boolean variables.
* Improved performance in the model elimination proof procedure due
to better caching (following a suggestion from John Harrison).
* First-order substitutions are now fully Boultonized.
* The first-order logical kernel makes local tweaks to keep proofs
as small as possible.

Initial check-in of the Metis first-order prover.