Progress with efficient evaluation of ``valid_ptree mmlG``
Handle the "fn v => e" form.
Handle parsing of patterns.

Still to handle translation/conversion to ASTs.
Start of work on converting pattern parse-trees to ASTs.
Complete conversion of pattern-parse trees into ast_pat type.
Parse top-level declarations (with some test-cases)
Convert top-level declarations into Ast_dec values.
An approach to handling optional semicolons at the end of declarations.

I don’t believe this to be ideal; in particular, it doesn’t handle

  let ; in 3 end;

which is valid SML.
Update hol-light scripts for recent changes to HOL

Specifically, move some OpenTheory mappings into HOL, and deal with the
removal of EVERY2.
New grammar for handling declarations in a more SML-ish fashion.
Changes to parse decl. sequences, both inside let and at top-level
Handle conversion to Asts of top-level decl. sequences.
Make tests fail if ast-conversion doesn’t give back an answer.
Complete handling of declaration sequences and semi-colons therein.
Use EVAL to check parse-tree validity (much faster).

Have to rewrite some theorems to get rid of existential quantifiers
and use various destructors instead.
Correct a bunch of problems in lexer_fun.

Mostly to do with primes and type variables, but also including some
token misidentifications.
Define a tokens->ast parseDecls function in mmlParseTheory.
Define an isWhitespaceT predicate.
New stringAST function to turn a string into a list of ML declarations.
Fix definition of lexical syntax for type variables.

Following discussions on mlton/polyml mailing lists with Andreas
Rossberg.