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

[Andreas Lochbihler]

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