Florian Haftmann wrote:
> Since this is part of the syntax layer,
>
> val unit = (fn Const (@{const_syntax Product_Type.Unity},__) => true |
> _ => false);
>
> is the appropriate antiquotation.
Thanks.
It's not entirely satisfying (I was hoping I could get away with not
mentioning Product_Type), but better than what I had before. I'll commit
this then.
> \<^const> indicates authentic constant syntax.
Ok. Now (I think) I understand the NEWS entry about authentic mode ;-)
NEWS on its own really is sometimes too cryptic.
Cheers,
Gerwin
