[isabelle-dev] find_theorems raises UnequalLengths exception

Tobias Nipkow nipkow at in.tum.de
Fri Nov 19 14:58:07 CET 2010

Thanks. Just for the record: the code eta-expands terms on the fly, but
the presence of beta-redexes may well confuse it.


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