[isabelle-dev] record pretty printing

[Gerwin Klein]

The pretty printing in the record package is currently broken.

Things like term "(| x = 0 |)" get printed as "(| x = 0, ... = () |)", i.e. 
the "more" component is not suppressed when it should.

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.

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.

Any bright ideas?

Gerwin