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