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

[Stefan Berghofer]

Quoting Lawrence Paulson <lp15 at cam.ac.uk>:
> But I could be wrong, as such checks may be done elsewhere. Does  
> anybody else have a suggestion?

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.

Greetings,
Stefan