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.