On 06/04/17 09:29, Lars Hupel wrote:
> while poking around in the function package (to store more information
> in "info"), I also realized that I need a little bit more information
> from the inductive package.
>
> Reading its sources, I stumbled upon 10-year-old comments by Makarius
> that remind the reader of (what I assume is) non-canonical use of global
> constant names in a "Generic_Data" slot.
>
> I took a stab at changing this to use item nets (as it is done in the
> function package). The draft patch is here:
Did you encounter an actual problem from that situation?
Formally, a comment is not a problem. "Fixing" such things prematurely
is likely to break it.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
