gmaxwell answered it: a large majority of mining power switched to running 0.7 -- which meant restarting the miners and clearing their memory pools. With the right dynamics, a rebroadcast would not repropagate because most nodes had not been restarted and would not rebroadcast it. Thus, those miners that restarted, started mining without it, and accepted the double-spend as a first-spend.
gmaxwell and gwillen just enlightened me a little further on #bitcoin-dev. The scenario seems likely to me now especially after I got the info that only about 10% of the miners had been on 0.7 before the split. They probably had the initial TX, but just didn't find a block in time.
I also understand why the 0.7 chain was chosen: if the 0.8 chains was chosen, double-spends would even now still be possible against merchants who are still asleep about the issue, which is worse.
A question still: rebroadcast? How does that work? Who would rebroadcasts the tx and triggered by what?
That particular theory, if correct, suggests that it's safer to have saved memory pools between loads, to make the keep/drop decision deterministic.
Saved memory pools, or maybe something in the protocol that enables syncing of the mempool from other peers? Sounds good, but again I don't know enough.
EDIT: fixed 0.7/0.8 mixup
