[isabelle-dev] Fwd: status (AFP)
bulwahn at in.tum.de
Fri Apr 8 13:45:53 CEST 2011
On 04/08/2011 01:03 PM, Stefan Berghofer wrote:
> Quoting Lukas Bulwahn <bulwahn at in.tum.de>:
>> 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?
Thanks for your effort.
I have already fixed the error (on my local machine) -- it was actually
related to some exception handling that has never been working, but was
never triggered before this changeset.
More information about the isabelle-dev