That is certainly my change, but I don't understand why preventing self-referential type instantiations should affect the find_theorems function. Can you get a full trace back from the exception?
Larry On 18 Nov 2010, at 16:03, Brian Huffman wrote: > 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 > _______________________________________________ > Isabelle-dev mailing list > Isabelle-dev@mailbroy.informatik.tu-muenchen.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev