citp embed

:embed (<label> ... <label>) as <module_name>

Incorporate proved goals into the module specified by <module_name> which will import the current proof context module.