I can't see an obvious bug in your code, but it's suspicious that the failure is caused by a theorem of the form "bot x = bot". Changing the code indeed corrects this error. I'm just running some tests now before pushing the change.
Larry On 19 Nov 2010, at 13:58, Tobias Nipkow wrote: > Thanks. Just for the record: the code eta-expands terms on the fly, but > the presence of beta-redexes may well confuse it. > > Tobias > > Lawrence Paulson schrieb: >> 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. _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
