This fix solves the problem with the exception. I tried it with 574613b47583.
Can you add it to the repository as I do not have wirte access to that.
Thanks,
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.lochbih...@kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
