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:
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?
isabelle-dev mailing list