The FM translation technology should rather use notation (pattern) for
mapping to TeX than the symbol level, because one Mizar symbol can have
very different contexts of use, and possibly very different TeX notations
(I think we already talked about this one with Grzegorz some time ago).
In FM translation the only almost but not quite unlike stable resource is
used:
formats (symbol+arity). For example, plus in expressions x+y, x+, +x etc.
may have different presentation in LaTeX. Namely, the first and third pluses
are
represented just by + but the second by ^+
Of course, there are bigger differences in translation for other symbols.
Patterns uses types of arguments annotated with constructors which change
from
version to version of distribution. Maintenance of translation patterns based
on
such resource may be quite interesting.