[isabelle-dev] Global constant names in inductive

Lars Hupel hupel at in.tum.de
Thu Apr 6 09:29:13 CEST 2017

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?


More information about the isabelle-dev mailing list