[isabelle] How do I make notation work only on the constant instead of on the type as well?



Dear Isabelle Users,

I'm on Isabelle 2009-2, and I'm stuck with the following problem. I have a structure whose constructor name is the same as its type. For presentation in LaTeX I'm using a notation hack which makes constants a different font than normal isabelle text.

Here's the problem. I define notation as:

notation (output)
  blah_C ("moo")

then:
	typ "('a, 'p, blah_C) ptr_t"
prints:
	('a,'p,moo) ptr_t

and: term "blah_C x y z" prints: "moo x y z" :: moo

Why does output notation pick up on the type, when I'm not using a type translation? How do I specify I want the constant blah_C as the target of my notation and not the type?

I realise that the same constructor and type name is not ideal, but the output does not come from a tool written by me.

Sincerely,

Rafal Kolanski.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.