[isabelle-dev] find_theorems raises UnequalLengths exception

[Brian Huffman]

Hello everyone,

Recently I noticed that in HOLCF, whenever I do a theorem search for
theorems containing the constant "UU" (i.e. bottom), the search fails
with an UnequalLengths exception. I tracked the problem down to this
specific theorem from Fun_Cpo.thy: Before this point, find_theorems
"UU" succeeds, and afterward it causes an error.

lemma app_strict: "UU x = UU"

I found that I can also reproduce the problem directly in HOL:

theory Scratch
imports Orderings
begin

find_theorems "bot"

lemma bot_apply: "bot x = bot"
by (simp only: bot_fun_eq)

find_theorems "bot"

*** exception UnequalLengths raised
*** At command "find_theorems"

After doing "hg bisect", I traced the origin of the problem:

http://isabelle.in.tum.de/repos/isabelle/rev/b654fa27fbc4

Can anyone figure this out?

- Brian