Keeping notation sane is, of course, very important. I think keeping notation sane is harder than it might first appear, but it is certainly possible.
One interesting trick used by Metamath's set.mm is to define variables that look similar to operators but can be defined for purposes of a particular proof (e.g., as hypotheses). For example, + underline, * underline, and so on.
For an example, see theorem grpridd, "Deduce right identity from left inverse and left identity in an associative structure (such as a group)." http://us.metamath.org/mpeuni/grpridd.html - the hypotheses include statements about "+ underscore", and lead to a proof about + underscore.
It has been a while since I worked with Isabelle locales. So how come that in your example "x + y" is not being confused with "A + B", although all involved entities are ZF sets? Or does A actually have a different type than x ?
Nevermind, I know the answer to that. That's why Set theory notation is a difficult problem, and you need some sort of type presentation / input layer. Some people also refer to that as a user space type system or soft types: https://www21.in.tum.de/~krauss/publication/2010-soft-types-...