> I'm at a loss for an explanation. Does anybody have any idea what is > going on there?
I now have an updated patch that instead of changing "add_inductive_global" to use "open_target"/"close_target" leaves it unchanged. With this, HOL-Proofs-Lambda and everything else goes through. <https://isabelle.in.tum.de/repos/testboard/rev/20d5e446aa10> Does anybody have any objections to pushing this? Cheers Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev