[isabelle-dev] Global constant names in inductive

[Makarius]

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