Fixing bug #3541.

All superscript numbers are now symbols instead of parts of identifiers.
This disallows some identifiers, but hopefully not a lot of people were
using superscripts as part of identifiers, weren't they?