[isabelle] Problems with datatype_compat



Dear all,

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"):
dest_prodT
(('a ttree × 'b) list tree × 'd) list


However, both datatypes are easily declared using the old datatype package:

datatype 'a tree = Empty | Node 'a "'a tree list"
datatype 'a ttree = TEmpty | TNode 'a "'a ttree list tree"


The problem occurs with both Isabelle2014-RC1 and -RC2.
The datatypes can be also be found in $AFP/thys/Datatype_Order_Generator/Derive_Examples.

Kind regards,
René



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.