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

[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