> 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.
Does anybody have any objections to pushing this?
isabelle-dev mailing list