[isabelle-dev] Global constant names in inductive

[Lars Hupel]

> 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