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 @Makarius: What is the rationale behind disallowing the definition of c? Or is this not an expected behavior? Dmitriy > On 31 May 2018, at 11:17, Blanchette, J.C. <j.c.blanche...@vu.nl> wrote: > > Hi Lars, > > Thanks for the heads-up. Makarius's change e0cd57aeb60c is clearly the > immediate source of the problem, but the more profound cause seems to be some > nonstandard handling of variables. The "illegal fixed variable" in question, > "s1", seems to originate from line 397 in "bnf_fp_n2m.ML": > > |> Variable.add_fixes (mk_names n "s") > > Dmitriy, since this is your code, could you take a look at it? The line in > question seems to have been added as part of an optimization you did in 2016 > (see 8053ef5a0174). > > Cheers, > > Jasmin > >> On 31. May 2018, at 10:28, Lars Hupel <hu...@in.tum.de> wrote: >> >> since approximately Isabelle/e0cd57aeb60c (~1 week): >> >> *** Malformed global fact >> "Misc_N2M.linorder_class.f1_t.n2m_t_ctor_fold_dict" >> *** Illegal fixed variable: "s1" >> *** At command "primrec" (line 164 of >> "~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy") >> _______________________________________________ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
