On Mon, 30 May 2011, Andreas Lochbihler wrote:
This fix solves the problem with the exception. I tried it with 574613b47583.
Can you add it to the repository as I do not have wirte access to that.
Thanks,
Andreas
Lawrence Paulson schrieb:
Thank you for looking there! This is the most plausible culprit. But it is
strange that this problem has arisen before.
A possible fix is to replace the last line of the function timing_depth_tac
in that file as follows:
handle PROVE => Seq.empty | THM _ => Seq.empty;
Andreas, do you want to try this and see if it helps?
Did anybody actually understand the source of the problem? The changelog
of c46107e6714b claims a "fix" without any explanation what was broken. A
spurious THM exception could have a quite unexpected cause.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
