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

Lawrence Paulson lp15 at cam.ac.uk
Fri May 27 16:32:16 CEST 2011

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?


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.

More information about the isabelle-dev mailing list