[isabelle-dev] find_theorems raises UnequalLengths exception

[Makarius]

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