[isabelle-dev] Fwd: [isabelle] Exception in conv.ML

Andreas Lochbihler andreas.lochbihler at kit.edu
Thu Jun 9 14:37:09 CEST 2011

I am afraid, no. Larry's fix solved the problem for me, so I did not dig any deeper.


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: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum 
in der Helmholtz-Gemeinschaft

More information about the isabelle-dev mailing list