[isabelle-dev] bug report: constant syntax for datatype constructors

[Makarius]

On Wed, 25 Mar 2009, Brian Huffman wrote:

> I noticed recently that datatype constructors don't get proper constant 
> syntax, for example:
>
> datatype foo = Foo foo | Bar
> ML {* @{const_syntax Foo} *}
>> val it = "Foo" : string

This is not a bug, just a feature: it is the old-style "non-authentic" 
syntax.  Only the newer packages, those based on local theories, declare 
authentic constants.


> Compare this with:
>
> definition "Foo = Suc"
> ML {* @{const_syntax Foo} *}
>> val it = "\\<^const>Scratch.Foo" : string

Here we have the new authentic syntax.  Many authors of old translations 
would consider it a bug ...


> This causes problems if I declare notation for a datatype constructor 
> using "notation", and later hide the constructor function using "hide 
> (open) const".

There are many problems like this with old-style syntax, but switching 
everything to authentic syntax in one big swoop will cause much greater 
trouble. In the past 2 years we have already eliminated a fair amount of 
old syntax, and this will continue, but requires great care.


 	Makarius