[isabelle-dev] SML/NJ happiness

[Makarius]

Isabelle/5e01e32dadbe is the result of spending some hours with SML/NJ and 
the ever growing HOL image.  In the end it turned out as rather trivial 
thing: Time.+ needs to be used in this qualified manner, since the adhoc 
overloading of + on different ML systems works differently.

I can't say on the spot why isatest gave uninformative "exception Option 
raised" here for almost two weeks, but it was relatively easy to see the 
point of failure in the mira reports.


SML/NJ might appear like a cruel tool for torture now, but it is just a 
look back in time.  10 years ago, SML/NJ and Poly/ML were almost equal in 
performance, and SML/NJ had slightly better error messages than Poly/ML.

The difference is that a lot of work has been done on Poly/ML and its 
integration into Isabelle (both Isar and Prover IDE), to make the comfy 
chair really comfortable.


 	Makarius