[isabelle-dev] ~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy broken

[Blanchette, J.C.]

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 <hupel at 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev