Reviving this old thread, Peter and me found out what is actually going on here.
Basically, nothing wrong. When abbreviations are declared, terms are
checked such that no abbreviations themselves are expanded. So in the
examples, the do-syntax produces an abbreviation bind_do which in this
case is not unfolded and so does not trigger the adhoc-overloading
disambiguation of bind. So, there is nothing wrong here.
Even more, given the analogy that ad-hoc overloading represents some
kind of overloaded abbreviations, adhoc-overloading should never be
expanded while abbreviations are checked (query
Proof_Context.abbrev_mode). @Christian. You might consider to adjust
your code accordingly after a second round of thinking about.
Cheers,
Florian
On 13.10.2013 17:36, Florian Haftmann wrote:
>>> Here a bisect would be helpful when this came to happen
>>> actually (or is it already present in Isabelle2013).
>>
>> This one already goes wrong in Isabelle2013.
>
> OK. I guess it is some variant of the ever recurring problem of »hidden
> polymorphism«. Will take some time to figure out actually.
>
> Florian
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> [email protected]
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
