[isabelle-dev] find_theorems raises UnequalLengths exception

Lawrence Paulson lp15 at cam.ac.uk
Fri Nov 19 15:05:59 CET 2010

I can't see an obvious bug in your code, but it's suspicious that the failure is caused by a theorem of the form "bot x = bot". Changing the code indeed corrects this error. I'm just running some tests now before pushing the change.


On 19 Nov 2010, at 13:58, Tobias Nipkow wrote:

> Thanks. Just for the record: the code eta-expands terms on the fly, but
> the presence of beta-redexes may well confuse it.
> Tobias
> Lawrence Paulson schrieb:
>> I'll give it a try.
>> Larry
>> On 19 Nov 2010, at 13:46, Tobias Nipkow wrote:
>>> The code is mine and I haven't looked at it for some 15 years. I agree
>>> with Larry, there must be some undocumented precondition about the form
>>> of the terms, eg that they are eta expanded or contracted. Presumably
>>> the calling context used to ensure those preconditions (otherwise we
>>> would would have seen the execption before) but does no longer. Larry's
>>> fix seems fine: it replaces a low level exception by the proper
>>> exception of that module but does not modify the unexceptional behaviour.

More information about the isabelle-dev mailing list