[isabelle-dev] Fwd: [isabelle] Exception in conv.ML
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
More information about the isabelle-dev