I don't have a small reproduction of the issue, but if you use bin/Holmake --qof with HOL4 at SHA1 6bf2bfd with the following file on a quiet (without much else running at the same time) Macbook Pro (OSX 10.11.6)

open HolKernel boolLib bossLib Parse val _ = new_theory"foo248" val _ = Define`foo a b = a < b` val _ = overload_on("<:",``\a b. foo b a``) val _ = export_theory()

then you will almost certainly get the following error out of Poly:

Run out of store - interrupting threads

The file is being read into Poly through a custom use function with its own lexer (to handle the backquotes) with calls to PolyML.compiler.

If you add a semicolon at the end of the second line, you don't get the error. With just a bit of load, the error is harder to get.

Michael