[isabelle-dev] Fwd: status (AFP)

Lukas Bulwahn 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>:
>> 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?

Hi Stefan,

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.


> Greetings,
> Stefan

More information about the isabelle-dev mailing list