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

[Lawrence Paulson]

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?

Larry

On 27 May 2011, at 15:27, Stefan Berghofer wrote:

> Hi Larry and Andreas,
> 
> there is another occurrence of gconv_rule in Provers/blast.ML
> (in function timing_depth_tac). Since the exception is thrown
> when invoking blast, this occurrence of gconv_rule may be the
> culprit.