I finally installed the newest MML and mizar binaries and found, to my
surprise, that new errors in my articles were introduced; the errors
were different from the ones that I might have found out about by
studying the above discussion. I found that that what used to be the
definition of the predicate "in" for 1-sorted structures moved from
RLVECT_1:def 1 to STRUCT_0:def 5. (Curiously, the definition
RLVECT_1:def 1 doesn't even exist anymore, that is, it doesn't seem
that it refers to anything, not just that the referent has changed!)
This was a minor though annoying problem to deal with. How could I
have known about this in advance? Perhaps a better summary of the
changes to the MML should be available, or maybe a script that one
could run on one's mizar articles that would make them conform to the
newest MML (as far as possible).