I didn't study a lot about what happen but I don't see how two different transactions with same hash can be spent, because of the uniqueness of txids
It's very simple. If it has the same ID, then it must have everything else also the same - pk_script(s), the value(s)... whatever So it doesn't matter which one of the two gets into an actual input while being spent, since they are both identical.
You have an index of unspent outputs, where each key consists of 36 bytes (TXID+Vout).
Now when you have a database that allows you to have duplicate indexes - then you just don't need to do anything. When you see the same TXID being mined, you just append it to the table. When you spend it, just make sure to delete only one record from it.
But if one day you switch to a database engine that enforces you to use a unique indexes - then you have a problem. Not a big one, you can work around it by adding a count filed to the unspent record, but nobody bothered.
It's OK that nobody bothered, it wasn't worth it, but my point is that blaming your (a developer's) problem on "broken miners" is just not fair, since they were not broken, but 100% protocol compliant at that time.
So yeah, since you used this word already, IMO you did steal that coins, and that is why when this, as you call him, "broken miner" would realize it one day, he should be entitled to a refund
