[isabelle] TYPE_MATCH exception with adhoc_overloading

Dear experts on adhoc overloading,

When I want to instantiate variables in a theorem using the attribute "of", sometimes the exception TYPE_MATCH gets raised. This seems strange to me because I would expect that adhoc_overloading either complains about not being able to uniquely resolve an overloaded constant or exchanges the constant in the AST.

By adding more type annotations, I have so far been able to circumvent the exception, but there seems to be a check missing. Attached you find a small example.


Attachment: Scratch.thy
Description: application/extension-thy

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