[isabelle-dev] record pretty printing

[Florian Haftmann]

> It all comes down to the line
> 
>     val unit = (fn Const ("Unity",_) => true | _ => false);
> 
> in HOL/Tools/record_package.ML which doesn't match Unity correctly.
> 
> Unfortunately, replacing it by @{term "Unity} or @[term "()"} doesn't work.

Since this is part of the syntax layer,

	val unit = (fn Const (@{const_syntax Product_Type.Unity},__) => true |
_ => false);

is the appropriate antiquotation.

> What does work is replacing it by "\\<^const>Product_Type.Unity", but that 
> feels very ad-hoc to me (I'm not sure where the \<^const> comes from), so I 
> haven't committed it yet.

\<^const> indicates authentic constant syntax.

Hope this helps
	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: florian.haftmann.vcf
Type: text/x-vcard
Size: 654 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20080213/0ba24669/attachment-0002.vcf>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 185 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20080213/0ba24669/attachment.sig>