[isabelle-dev] Fwd: status (AFP)

[Lukas Bulwahn]

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.

Lukas


> Greetings,
> Stefan
>