[isabelle-dev] Forgotten feature of the datatype package

[Brian Huffman]

Hi all,

Lately I've been trying to update the HOLCF domain package to make its
design and features more consistent with the datatype package. 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".

The syntax of the datatype command allows an optional string in
parentheses, which is supposed to be used for the qualified names of
constructors, lemmas, etc. in place of the actual type name. Here's
the relevant parser from HOL/Tools/datatype_package.ML:

val datatype_decl =
  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args --
P.binding -- P.opt_infix --
    (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ --
P.opt_mixfix));

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.

I'd like for the HOLCF domain package and the datatype package to have
similar features and syntax, as much as possible. So should the domain
package copy this old feature, or would it be better just to remove it
completely?

- Brian