How to hide multiply defined constants

Question

This questions extends the question How to hide defined constants.

I import theory A, B, and C, maybe in future also D, E, ... All theories define a function f. I want to hide the definition of f in my current theory without changing the imported theories. When I write term f I get A.f. When I add hide_const (open) f to my current theory, A.f is hidden but now I get B.f as f. How can I completely hide f? I need something like (hide_const (open) f)+.

Answer 1

The versions of function f from each theory have separate names (A.f, B.f, C.f), and these must all be hidden separately.

You are allowed to hide multiple names with a single hide_const command, though, and this is what I would recommend:

hide_const (open) A.f B.f C.f