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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
