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

[Andreas Lochbihler]

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

Andreas

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
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum 
in der Helmholtz-Gemeinschaft