[isabelle-dev] Datatype alt_names

[Alexander Krauss]

Makarius wrote:
> Grepping through the sources for alt_name right now, I get the 
> impression that there was a second motivation: make really sure that the 
> synthesized "big_rec_name" variations really work in the target 
> context.  Due to loss of information in base_name, it could in principle 
> clash with other names bound in the same context.

The generated names do use the alt_names component if available, but 
this does not really prevent clashes, since empirically, the alt_names 
field always contains either NONE or the base names of the types, c.f.

ML {*
Datatype.get_all @{theory}
|> Symtab.dest |> map (apsnd #alt_names)
|> map @{make_string} |> cat_lines |> writeln
*}

So, at least currently, the alternative names are never really different.

Both datatype and rep_datatype seem to offer the possibility to specify 
different names here. For rep_datatype this is used once in 
Library/Bit.thy, but the name is actually the same. For datatype it 
seems to be broken anyway, as reported by Brian.

So it seems that this can be safely eliminated, unless some other 
package uses it via the ML interface, which should be easy to check.

Alex