Remove obsolete comment about (!!)

as spotted by David Feuer and reported as #9585.
The comment was right until ceb68b9118fa883e88abfaa532fc78f6640cf17f,
which is only 13 years ago :-).