[isabelle-dev] find_theorems raises UnequalLengths exception

[Tobias Nipkow]

The idea was that that code would be incomplete but not incorrect
outside the HO pattern term language. But indeed, th actual code has not
been verified...

Tobias

Makarius schrieb:
> On Fri, 19 Nov 2010, Tobias Nipkow wrote:
> 
>> Just for the record: the code eta-expands terms on the fly, but the
>> presence of beta-redexes may well confuse it.
> 
> It is known for many years that the pattern unification does have
> occasional problems with beta redexes.  This is one of the things that
> have never been touched so far because other problems might lurk in the
> dark, and the whole thing is critical for the correctness of the kernel.
> IIRC, I have discussed it with Stefan Berghofer the last time about 5
> years, and he could not explain to me the exact situation.
> 
> 
>     Makarius