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

Added a few newlines at end of files to suppress warnings from my
Mosml -> MLton preprocessor.

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.

Gave this module a signature file, with documentation, and also fixed a
bug found by Mike; OmegaSimple was making the classic mistake of using
the global grammar to do its parsing.

Progress with Omega. Also refactored code for handling natural numbers
and generalising over non-presburger sub-terms so that both Omega and
Cooper can use it.

More hacking 'round in search of extra efficiency. Really though, it's
too early for this. Have developed some more useful primitives in
OmegaMath though.

OmegaSimple.simple_CONV takes a closed problem in normalised form, i.e.,
?x1 ... xn. cst1 /\ cst2 /\ cst3 .. /\ cstn
where each csti is further of the form
0 <= c1 * v1 + c2 * v2 + ... + cn * vn + n
and attempts to prove the problem true or false by using the ML shadow
code. Code seems to work, and various tweaks to OmegaMath mean it is a
little quicker than it used to be.

This file will try to use the ML Shadow code to quickly prove closed
existential formulas.