[isabelle-dev] find_theorems raises UnequalLengths exception

[Lawrence Paulson]

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.