On 01/06/18 10:35, Dmitriy Traytel wrote: > Hi all, > > thanks for pointing this out, Lars. And thanks for looking at the sources, > Jasmin. > > The problem seems to only show up when the declaration in question is inside > of a class context. Here is a reduced version that does not involve primrec > at all. > > context linorder begin > > context fixes b :: nat begin > > definition c where "c = b" > > end > > end
This is ultimately a problem of the class target in conjunction with the unnamed local context. See now changeset: 68351:bcdc4c21ab1d tag: tip user: wenzelm date: Fri Jun 01 22:01:43 2018 +0200 files: src/Pure/Isar/class.ML description: varify frees, notably dangling_params (see also e0cd57aeb60c); > @Makarius: What is the rationale behind disallowing the definition of c? The changeset explains it as follows: changeset: 68239:e0cd57aeb60c user: wenzelm date: Sun May 20 22:37:00 2018 +0200 files: src/Pure/global_theory.ML description: more checks for global facts: disallow undeclared frees (as in Export_Theory.export_fact); At first I did not want to expose odd mixtures of free vs. schematic variables to the world out there, and for global items we have a clear understanding that fixed vs. schematic can always be flipped via Logic.varify_global/unvarify_global and related operations. Moreover, the check was meant to tighten existing tools and local theory targets, as we have seen here. In the process, I had to give up the full rigour, though: a3bd410db5b2 allows mixed variable indexes. Looking even more closely at global facts, there might be further problems that are still undetected. In the next round I will experiment with Thm.plain_prop_of to see if we can disallow hyps, shyps, tpairs. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev