clarified export of formal entities: name space info is always present, but content depends on option "export_theory";