[isabelle-dev] Type arguments in datatype declarations

[Florian Haftmann]

Hi Stefan,

> why can't we repair interpret_construction so that it handles this case
> properly?

well, we can extend interpret_construction in such a way but also have
to do so for the tools which use it.  This is perhaps not even that
difficult, but it adds considerable complexity to already complicated
tools, only to keep codified comments (the only effect of different
names of type variables in datatype branches is in the theory source
text and some quasi-internal tables).

> Nevertheless, it would be interesting to see what goes wrong,
> since your example used to work in older releases of Isabelle without
> further ado.

This surely is worth the effort.

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20100927/d5c58ab2/attachment.sig>