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
