[isabelle-dev] Type arguments in datatype declarations

[Stefan Berghofer]

Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

> thanks for this offer.  But this misperception has not only infected
> size but all datatype tools using the
> Datatype_Aux.interpret_construction combinator which assumes exactly the
> same restriction.  Therefore my proposal to internally provide a
> consolidated view of the datatype specifications with type parameter
> names made uniform, to handle the issue at one place and not in every
> datatype package extension separately.

Hi Florian,

why can't we repair interpret_construction so that it handles this case
properly? Nevertheless, it would be interesting to see what goes wrong,
since your example used to work in older releases of Isabelle without
further ado.

Greetings,
Stefan