[isabelle-dev] Problems with datatype-new

[Jasmin Christian Blanchette]

Hi René,

> I have an unexpected problem when defining a datatype using datatype_new.
> 
> theory Test
> imports  
>  "$AFP/Collections/ICF/impl/RBTSetImpl"
> begin
> datatype_new ('a,'b) bar = Foo 'a "'b option" "'b rs"
...
> Just wanting to report this,

Thank you for your report. This is now fixed (cf. 465ac4021146).

Cheers,

Jasmin