[isabelle] How do I retrieve the mixfix syntax of a constant?



Dear Isabelle Users and Gurus,

I have written a ML function which creates a new constant definition based on the type of an old one, for example, the _any transform:

definition
  "map_bp_any p ≡ λs. ∃v. map_bp p v s"
(where map_bp was also defined using "definition")

I also want to generate the appropriate mixfix syntax for the new constant. I know how to do the transformation and how to declare syntax, but I need to get the syntax for a constant, e.g. "map_bp". I've been grepping through the source but can't see anything that returns a mixfix.

In this case, I want to get out:
	("_ :→ _" [56,51] 56)
so I can turn it into:
	("_ :→ -" [56] 56)

Does anyone know how to do the syntax retrieval for a constant?

Sincerely,

Rafal Kolanski.






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