[isabelle-dev] record pretty printing

[Gerwin Klein]

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