# [MLton] MLton HOL

**Joe Hurd
**
joe.hurd@comlab.ox.ac.uk

*Fri, 2 Jul 2004 00:42:54 +0100 (BST)*

On Thu, 1 Jul 2004, Stephen Weeks wrote:
>* I also fixed one quadratic performance bug in our code generator that
*>* Matthew found. It turns out that this bug caused the bulk of the
*>* slowdown in the 8.6 hour compile. As a result, my latest compile of
*>* HOL took 1.3 hours.
*
This is great! I'll attempt to build MLton from CVS, and get back to
you if I have any trouble with this. Thanks for adding the exception
printer---that'll come in very useful.
I asked the HOL developers about a file format for theories, and their
main objection was that for interactive proof it's convenient to bind
theorems to ML identifiers. So my question to you is, assuming I have
read in a large collection of theorems to a suitable data-structure,
is it possible to write something like
val theorem_1 = DB.fetch "theorem_1";
val theorem_2 = DB.fetch "theorem_2";
...
val theorem_n = DB.fetch "theorem_n";
in such a way that it won't generate vast amounts of code and
variables in MLton?
Thanks for your help,
Joe