Re: [isabelle] Problems with datatype_compat

Hi René,

On 05.08.2014 18:27, Jasmin Christian Blanchette wrote:
Hi René,

Am 05.08.2014 um 12:20 schrieb René Thiemann <rene.thiemann at>:

I encountered the following problem when using datatype_compat:

datatype_new 'a tree = Empty | Node 'a "'a tree list"
datatype_compat tree

datatype_new 'a ttree = TEmpty | TNode 'a "'a ttree list tree"
datatype_compat ttree

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 MHonArc.