Elimination of Extended ASCII & new lexical traps

[Andrzej Trybulec <trybulec@wwwserve.cs.shinshu-u.ac.jp>]

Adam Grabowski eventually decided to remove from MML all extended ASCII 
characters (with codes >= 255).
They are replaced by new symbols, that may cause some troubles.

When updating an old article (not yet submitted) I got the error #103 
(unknown funtor) in an iterative equality:

       .= 1*p by REAL_2:12
::>          *103

Rather confusing (it is just real mutliplication, but ASCII #249 is 
substitued now by '*'). The problem is that I have in the lexical 
environment the vocabulary JORDAN2C on which '1*' is introduced as a 
symbol - it is used in the definition JORDAN2C: def 7,   1* n is finite 
sequence of reals consisting of n elements equal to 1.

To correct it I should put a space between '1' and '*', but
        .= 1 *p by REAL_2:12
does not look nice, even if it is correct.

I believe every Mizar user felt down in most famous lexical trap. If you 
write
     a+c=b+d
it is construed as
    a  +  c=   b  +  d
because 'c=' is the symbol for the inclusion (it is ever in the 
environment , HIDDEN.VOC)

A bit more original:

I had in a scheme formula

      P[x] & P[y] implies ...

and I needed the CAT4 vocabulary. But then I got an error at 'P[x]'. The 
reason: Czeslaw Bylinski introduced
'[x]'  as the symbol for the product in a category (CAT_4:def 5)

Regards,
Andrzej Trybulec