[MLton] HOL's Moscow ML implementation, and pushing MLton to emulate it

[Stephen Weeks]

> Now we just need that embedded SML interpreter for our script (=
> theory-generation) files.

One thing that occurs to me about the embedded interpreter is that it
will be used to develop code that will then transition to the
monolith, which is compiled by MLton.  So, it is important to have as
much compatibility between the languages used by the interpreter and
MLton as possible.  Because of differences between SML implementations
(mostly libraries, but sometimes language too), it may thus make the
most sense for the embedded interpreter to use MLton's front-end and
libraries.  One other argument for taking this approach is that many
other projects could benefit from having a MLton-compatible
interpreter.