[isabelle] Canonical types of constants



In order to obtain the type of a constant c I am using this code snippet:

Proof_Context.read_const {proper = true, strict = false} ctxt c

It gives me back a term Const(c,T) and then I proceed with T. How can I make sure that the type variables in T have canonical names 'a, 'b etc? Should I be using some other piece of code?

The background is that in 7f5579b12b0a, constant "card" has type "?'b set => nat" instead of "?'a set => nat" as in the past. I assume that I should not rely on canonicity of names in T? If not, how can I convert a type into a `canonical' one?

Thanks
Tobias

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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