On Thu, 9 Jun 2011, Lawrence Paulson wrote:
I see you are alert, as always!
Just the normal process of consuming incoming mails and changesets ... :-)
But here there were two reasons for extra attention: (1) suspicious
keywords in the log entry (like fixed or bug) and (2) a realistic
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
It looks like this exception is raised when gconv_rule cv i th is called and
the specified subgoal does not exist. The function gconv_rule is called in only
four places in Pure:
./Isar/element.ML: (Conv.gconv_rule Drule.beta_eta_conversion 1 r)
./raw_simplifier.ML: then Conv.gconv_rule
I'll be happy to provide a trace if you tell me how to obtain one. If I turn on
Debugging in the settings menu, I only get an empty exception trace in the
isabelle buffer:
Exception trace for exception - THM raised in conv.ML line 212
End of trace
Andreas
Lawrence Paulson schrieb:
It looks
Quoting Lawrence Paulson l...@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
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
