This question arose from something on the isabelle-dev list but I think it's really of general interest.
Currently Poly/ML only gives the "Run out of store - interrupting threads" message if it really cannot allocate the required memory after a full GC. This is actually rather unlikely for small cells. Instead as the amount of free space left in the heap gets smaller the GC runs more and more often. The ML code is still making progress but only very slowly. I wonder if there is a case for actually giving up at that point. Is it better to plough on in the hope that the program will complete or is it more helpful to produce a message and allow the user to try with more memory? This situation is most likely to happen if the heap space is restricted either because the address space limit has been reached in 32-bit mode or if the maximum heap has been set too low with --maxheap.
David