Dear BNF developers, it appears that the "datatype_compat" cannot cope with non-standard bindings. I get an "exception Bind" when trying to invoke "datatype_compat" on a "qualified" or "private" datatype. There's a somewhat satisfactory workaround, which is to use
setup ‹Sign.mandatory_path "some_prefix"› ... setup ‹Sign.parent_path› Cheers Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
