We were not ignoring double underscores for mnemonics in one place, as we should.
Fixes: #4129 (closed)