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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
