Replace BNFs with MRBNFs in Isabelle

[jvanbruegge]

This would make datatypes compose correctly with binder_datatypes

[dtraytel]

Is this related to #76? What is the issue of having two databases for BNFs and MRBNFs as we have now (prioritizing MRBNFs when looking up things)?

[jvanbruegge]

Have not had a look at #76 , but it is related to #72
The problem is if you nest a binder_datatype in a normal datatype (as in the context type in #72). This will make the datatype kill all free positions on the binder_datatype. If we replace the BNF axiomatization with MRBNFs, we could carry them through

[dtraytel]

I see. BTW, I was first confused why prepat has a dead variable in the first place but it is the sort constraint that makes it dead. However the sort constraint is not needed for the definition of the prepat. So a fix would be just to remove the sort constraint from the datatype declaration. (I haven't tried this—not at the computer atm.)

[jvanbruegge]

No that is not quite the reason. MRBNFs get registered as BNFs in their lives, we have to kill other positions bevause the map function has the wrong shape