Pushout operator does not elaborate constants into generated named theory's body

[rappatoni]

Example Code:

namespace http://mathhub.info/Panopikum/examples❚
import base http://mathhub.info/MitM/Foundation ❚

fixmeta http://cds.omdoc.org/urtheories?LFComb ❚

theory start : base:?NaturalDeduction =
A:prop ❙
B:prop ❙
ax: ⊦ A ❙
❚

theory out : base:?NaturalDeduction =
include ?start ❙
axi: ⊦ A ⇒ B ❙
❚

theory target : base:?NaturalDeduction =
include ?start ❙
C: prop ❙
D: prop ❙
axone: ⊦ C ❙
❚

view re : ?start -> ?target =
include base?NaturalDeduction ❙
A = C ❙
B = D ❙
ax = axone ❙
❚

diagram pushout : http://cds.omdoc.org/urtheories?LFComb := PREFIX PUSHOUT ?out ALONG ?re BY "pushout_" ❚

theory proof =
include ?pushout_pres ❙
beweis: ⊦ D ❘= MP axi axone❙
❚

This will produce a theory with an empty body. The generated constants remain stuck in the theory's definiens.

[ComFreek]

This will probably vanish into thin air during the reimplementation of diagram operators that @florian-rabe planned.