Maybe it’s time. They’ve not made it better, and it seems pretty hopeless now. Larry > On 31 Jan 2016, at 13:41, Makarius <makarius at sketis.net> wrote: > > We could discontinue ML_SYSTEM_POLYML and merely test the "HOL" session for SML/NJ. > > Or we could discontinue SML/NJ altogether. I proposed that the last time 10 years ago.