Everywhere remove use of temp_set_grammars idiom for setting up the
local grammars, preferring instead to statically bind the appropriate
names. You need to grab Parse.Term and Parse.Type as well as Term and
Type, requiring the definition of a Parse structure.

Follow-on fixes to changing Term to Parse.Term and Type to Parse.Type
in the quotation pre-processor. A mass of trivial changes, but the
new way of dealing with files containing code that does parsing
(not script files) is to

* grab the ambient grammar(s)
* set the current grammar(s) to the right values
for parsing quotations in the file
* the body of the file
* reset the current grammar to the ambient grammar

For an example, see src/taut/tautLib.sml

Got rid of QConv, and made all conversions do the "raise exception to
indicate reflexivity" thing. (Also fixed bug in new implementation
of ABS_CONV that attempted renaming on failure of conv, and not just
failure of ABS.)

Next step will be to rework the simplifier's implementation so that
it also uses Conv.UNCHANGED, rather than in its own internal version
of the same. This will let the simplifier play efficiently with
others.

May also assess making ABS_CONV not do renaming, and give the rewriter
its own special traverser. This might make some things more efficient.

Omega now passes all of its tests, and I claim it's probably now a reasonable
approximation of a complete procedure for doing Preburger arithmetic.
Aggressive preprocessing attempts to minimise DNF blowup, but the fact
that EXISTS_OR_CONV can still consume over 10% of the procedure's running
time basically sucks.

OMEGA_CONV is now "almost complete". There are just bugs to be ironed out.
Changes are too many to document extensively. Some though:
* OmegaMath has got a lot bigger, with OmegaEq being merged into it and
also gaining some divisibility normalisation code.
* couple of new test cases
* decided against prenexing mixed quantifier problems.

Moved some theorems about; basic machinery is now in place to decide all
problems with only one sort of quantifier (occasionally the out-of-the-logic
approach breaks, and the symbolic approach is needed, even for all-one-
quantifier problems).

Implemented two more optimisations for "simple Omega". One made
the noxious SUNRISE example go twice as fast. (It's still almost three
times faster if you use Cooper though.)

The first optimisation made the contextual simplification smarter, while the
second took the opportunity to do single-point elimination before converting
to DNF where possible.

Revisions to the code that DNF-ifies the problem set, including a phase
of "congruential simplification". On those problems that Omega can get
it seems quicker than Cooper in almost all case. One very notable
exception suggests that there is still work to be done though.