Hi Makarius,
> On 1 Jun 2018, at 23:32, Makarius wrote:
>
> 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
>>
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
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
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":
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")
