On 06/04/17 13:08, Lars Hupel wrote: >> Did you encounter an actual problem from that situation? >> >> Formally, a comment is not a problem. "Fixing" such things prematurely >> is likely to break it. > > Yes, there is an actual problem. I define a function via > "Function.add_function" and inspect the resulting info. As per usual > discipline this looks as follows:
> That is, I inspect the relation as generated by the function package. > The termination proof needs to get some information about that relation > from the inductive package. However, "#R" is a term, not a const name > string. Before I close the target, it will be a free variable. OK, that is a better motivation. Your proposed change https://isabelle.in.tum.de/repos/testboard/rev/20d5e446aa10 looks formally OK. My old comment from 10-years ago stems from: changeset: 25380:03201004c77e user: wenzelm date: Sat Nov 10 18:36:08 2007 +0100 files: src/HOL/Tools/inductive_package.ML description: put_inductives: be permissive about multiple versions (target names are not necessarily unique); add_inductive: store info under global (!) name -- very rough approximation of the real thing; That historical context is important. Isabelle development means to study sources + history carefully and to make empiric explorations against current applications (notably AFP). The date above reminds me of chaotic times in 2006/2007 when far too many things were changed without clear principles. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev