[isabelle] Problems with datatype definition

Dear all,

the following datatype definition is not accepted in Isabelle/HOL,
presumably since the parameter of foo has been changed to "'a option".

datatype 'a foo = Bar 'a | Com "'a option foo"

Is there some known workaround for this problem?

Thanks in advance,
René Thiemann                    mailto:rene.thiemann at uibk.ac.at
Computational Logic Group        http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck

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