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

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to