I am afraid, no. Larry's fix solved the problem for me, so I did not dig any
deeper.
Andreas
Am 09.06.2011 14:29, schrieb Makarius:
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
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: [email protected]
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
