Re: [isabelle] Problems with datatype_compat
On 05.08.2014 18:27, Jasmin Christian Blanchette wrote:
Am 05.08.2014 um 12:20 schrieb René Thiemann <rene.thiemann at uibk.ac.at>:
I encountered the following problem when using datatype_compat:
datatype_new 'a tree = Empty | Node 'a "'a tree list"
datatype_new 'a ttree = TEmpty | TNode 'a "'a ttree list tree"
exception TYPE raised (line 329 of "~~/src/HOL/Tools/hologic.ML"):
(('a ttree × 'b) list tree × 'd) list
The problem occurs with both Isabelle2014-RC1 and -RC2.
The datatypes can be also be found in $AFP/thys/Datatype_Order_Generator/Derive_Examples.
Thanks for the report! Dmitriy and I have been looking more closely at the issue but we haven't been able yet to determine if it's his bug or mine. ;) Hopefully we'll be able to come back to you in the coming days with a fix. Regarding the Isabelle2014 release, I fear we won't be able to include a fix, since this isn't a regression and we must be very conservative in our changes so close to a release.
As usual, sorry for the trouble.
It should be better now in Isabelle's repository version 9c065009cd8a.
The observed bug was mine, but your report triggered a cascade of
robustifications in both, mine and Jasmin's code. Thanks again!
This archive was generated by a fusion of
Pipermail (Mailman edition) and