Этот вопрос расширяет вопрос Как скрыть определенные константы.
Я импортирую теории A, B и C, возможно, в будущем также D, E, ... Все теории определяют функцию f. Я хочу скрыть определение f в моей текущей теории без изменения импортированных теорий. Когда я пишу term f, я получаю A.f. Когда я добавляю hide_const (open) f к моей текущей теории, A.f скрывается, но теперь я получаю B.f как f. Как я могу полностью скрыть f? Мне нужно что-то вроде (hide_const (open) f)+.
