[isabelle-dev] Additional type variable(s) in specification

[Brian Huffman]

On Thu, Dec 2, 2010 at 11:26 AM, Makarius <makarius at sketis.net> wrote:
> Back to history: in 2005 Brian had a paper on TPHOLs with a footnote about
> an unexpected crash of the typedef package due to hidden polymorphism in the
> set involved, not the type.

It was a simple error message, not a "crash".

> What I did then is to make the typedef package
> insert "itself" arguments in the way one would think of as a first idea.

*My* first idea was that "typedef" didn't need to be defining a set
constant at all.

>  This made the problem go away for the moment, although it complicated the
> package implementation.  When Larry was asking me about that change of
> typedef later, I also failed to explain to him both the problem and its
> solution.

I'm surprised that you bothered with such a complicated solution when
such a simple workaround existed -- the same workaround that I used in
that paper -- just use "typedef (open)". If the default behavior of
the "typedef" command was to work like "typedef (open)" (and I think
it ought to be), then there would have been no problem, and no need
for the footnote explaining what the "(open)" option means.

- Brian