[isabelle-dev] A possible bug with Isabelle 2013

[Lawrence Paulson]

In Edinburgh LCF, term quotations containing anonymous type variables were simply rejected. Perhaps that would still be the best approach now. I'm not convinced that it would lead to more errors than the 'a itself approach.

Larry

On 1 Mar 2013, at 11:35, Makarius <makarius at sketis.net> wrote:

> I actually had that in an early version of Isar around 1998/1999, but it turned out hardly usable without the Hindley-Milner type generalization within the proof text.  So I added that, while realizing the problem that was later formally called "hidden polymorphism".  Back then I had a slightly awkward indication of the excess polyorphism that would now cause much more surprise if it were still there.  When the 'a itself argument emerged as the standard way to represent that situation, I merely cleaned up that old code.