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:


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

Reply via email to