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
