[isabelle-dev] "spass": Internal error: exception Empty raised (line 458 of "library.ML")

[Jasmin Blanchette]

Am 24.04.2012 um 20:58 schrieb Makarius:

> have also made some more experiments.  The Empty exception is from the split_last here http://isabelle.in.tum.de/repos/isabelle/file/ea153f6abdb6/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML#l614 where you don't get any output unexpectedly, bacause /bin/sh has crashed. Ouch!
> 
> Such things happen on Cygwin.  I will try to sort out the physical problem.  Maybe you can make the ML part more informative nonetheless.

OK, it looks like we came to the same conclusion (see my email from one minute ago).

Jasmin