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

[Brian Huffman]

Hi all,

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

Compare this with:

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

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

I wouldn't mind fixing this myself, except that I'm not sure how to do it.

- Brian