[isabelle-dev] antiquotations and type_synonyms

[Tobias Nipkow]

I was under the impression that type synonyms are expanded in typ
antiquotations, but apparently not, at least not with 30624dab6054. If I write
@{typ vname} I get "vname", even if vname is a type synonym for string. Maybe it
has always been like this, but it means that one cannot automatically display
(in latex) what some type synonym stands for, one has to type it in. Conversely,
if they were expanded, one could always prevent that with the [source] modifier.
Any views on this?

Tobias