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
