Move generally useful to_vstruct function into Absyn

It was hidden in the TermParse module.

Move generally useful traverse function to Absyn structure

This function recursively transforms Absyn values in a top-down way,
and it was unnecessarily hidden in TermParse.

Extract Absyn datatype decl. into separate file

This removes redundancy and also gets the standard Poly/ML
pretty-printer in version 5.6 to print the values usefully, rather than
as "?".

Starting to remove redundant (and potentially error-introducing) infix
declarations.

Need infixr -->, otherwise prettyprinter gets confused and
doesn't print

\(x,y). x = 0

properly.

Alter the representation of Absyn.absyn and Absyn.vstruct to include
locations. Fill these in in Parse.sml and parse_term.sml as
appropriate. Make sure everything else still builds.

Simplified some proofs in MachineTransitionScript.

Reverted to Taupo-6 RW_TAC. This should make RW_TAC faster, and a little
less eager to case-split conditionals. Some proofs may break as a result.
In that case, use the drop-in replacement BasicProvers.NORM_TAC.

Term destructors now operate using same_const to check the operator
of the term being destructed. This may increase efficiency somewhat.
There were consequent changes to the xSyntax modules of the system.

Printing r1.fld1.fld2 was coming out as (r1.fld1).fld2. Blech.

Latest mods for making everything paired.

Changes to bring about Kananaskis parser. Known bug exists in
treatment of qualified identifiers.

Relatively radical changes to get rid of the preterm type that lived
in parse_term and replace it with a cleaner Absyn type that Konrad
wrote for TFL.