[isabelle-dev] Fwd: status (AFP)

[Stefan Berghofer]

Quoting Lukas Bulwahn <bulwahn at in.tum.de>:

> Hi,
>
>
> My changes caused this error.
>
> I am working on different compilation schemes in Quickcheck.
> Quickcheck registers its type-class based generator construction in the Datatype package in the HOL image.

Hi Lucas,

according to the trace, the exception occurs somewhere in the function
derive_datatype_props in datatype_data.ML. When taking a quick look at
the code, I noticed that thy2 is used in two places (lines 311 and 322)
after it has already been modified. Is that intentional, or could this
be related to this bug, too?

Greetings,
Stefan