[isabelle-dev] Forgotten feature of the datatype package

[Makarius]

On Fri, 22 May 2009, Brian Huffman wrote:

> I came across an old feature of the datatype package that doesn't work 
> anymore:
>
> theory Scratch
> imports Main
> begin
>
> datatype (bar) foo = Foo
>
> *** Unknown constant: "Scratch.foo.Foo"
> *** At command "datatype".

> I suppose this feature might be useful if for some reason you wanted to 
> define a datatype with a non-alphanumeric name. But obviously it is not 
> *that* useful, since the feature has been broken since Isabelle2008 at 
> least, and apparently nobody has noticed.

This still needs some further investigation.  As a general rule of thumb 
there is no need to imitate obscure features of old packages, if there is 
no clear indicating that there will be actual uses.

On the other hand, original 'datatype' as one of the very first Isabelle 
packages probably still depends on this feature internally.  IIRC, it was 
introduced to accomodate old-style type names such as "*" which will still 
be with us for some time.  In newer developments, those that are less than 
10 years old, plain identifiers are used uniformly of course.


 	Makarius