rw gives error message, but still works?

Stream: general

[Michael Stoll]

I have just encountered a situation where I have a goal of the form (a ^ 4) ^ 2 = 1, which I want to rewrite to a ^ (4 * 2) = 1, so I do rw ← pow_mul. It gives me the error message

rewrite tactic failed, did not find instance of the pattern in the target expression
  (?m_3 ^ ?m_4) ^ ?m_5

but when I move the cursor after the rw, it shows the goal as a ^ (4 * 2) = 1 (and at the end of the proof, "goals accomplished").
Is this a bug?