[isabelle-dev] Global constant names in inductive

[Lars Hupel]

Dear list,

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:

  <https://isabelle.in.tum.de/repos/testboard/rev/23d773b06377>

Unfortunately, this breaks HOL-Proofs-Lambda with a rather mysterious

  exception THM 1 raised (line 741 of "thm.ML"): assume: variables

I'm at a loss for an explanation. Does anybody have any idea what is
going on there?

Cheers
Lars