On 04/08/2011 01:03 PM, Stefan Berghofer wrote:
Quoting Lukas Bulwahn <[email protected]>:
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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
