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

Andreas Lochbihler andreas.lochbihler at kit.edu
Fri May 27 16:57:36 CEST 2011

I'll try this, but it will probably take until Monday.


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?
> 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.

Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum 
in der Helmholtz-Gemeinschaft

More information about the isabelle-dev mailing list