[isabelle] datatype_new_compat requires sort type



Dear BNF implementors,

I just want to report that in Isabelle2013-2, the datatype_new_compat command fails on datatypes that have been declared with sorts other than {type} on their type variables. Here's a small example.

theory Scratch imports "~~/src/HOL/BNF/BNF" begin

default_sort equal
datatype_new 'a foo = Foo 'a
datatype_new_compat foo

*** Type error in application: incompatible operand type
***
*** Operator:  fa :: 'a => nat
*** Operand:   x :: 'b
*** The error(s) above occurred in axiom "foo_size_def"
*** At command "datatype_new_compat"

Best,
Andreas




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