We had some duplicate mappings in mappings to start with. Now we have some
code to complain loudly about these, and all currently existing duplicates
have been dealt with.
We also had a problem where in some Python dict, existing stuff was using
strings as keys while new data would use numeric indices, thus not
overwriting the previous value. Now we always use strings as keys.
Along the road, the italic dotless i and j symbols were changed
so that they now are taken from cmmi10 instead of cmti10.
d26a67f220