[isabelle-dev] Fwd: [isabelle] Exception in conv.ML
makarius at sketis.net
Thu Jun 9 14:29:44 CEST 2011
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.
> 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.
More information about the isabelle-dev