[isabelle-dev] Notes on datatype_new list

[Jasmin Blanchette]

Am 26.05.2014 um 12:05 schrieb Makarius <makarius at sketis.net>:

> The observed here problem is different: the type constructor "list" somehow ends up in the name space with a "concealed" flag.  There might be one or more Binding.conceal too many in the BNF sources.

Ah, now I get it. Of course this is entirely accidental, and I'm surprised we didn't notice before. We'll look into this.

Jasmin