[isabelle] const antiquotation


I noticed a strange behaviour with the const antiquotation:

ML {* @{const "op ="} *} raises a TYPE exception.

I was hoping it would give me the HOL constant for equality. Is there some easy rule of thumb about when the const antiquotation works and when it doesn't?

(This is in both Isabelle-2009-2 and Isabelle-2009-1)


The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

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