[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"


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