[isabelle] datatype_new_compat produces illegal type



Dear BNF experts,

In Isabelle2013-1, I tried datatype_new_compat on the following example:

theory Scratch imports "~~/src/HOL/BNF/BNF" begin
datatype_new ('out, 'in) event = Event 'out 'in
datatype_new_compat event

Unfortunately, I get the following error upon datatype_new_compat:

*** Illegal type for constant "Scratch.event.event_rec" :: ('c => 'd => nat) => ('a, 'b) event => nat
*** The error(s) above occurred in axiom "event_size_def"
*** At command "datatype_new_compat"

What am I doing wrong here?

Best,
Andreas




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