@jesus2099: I am using isrcsubmit.py, which, in my case relies on cdrdao.
@Heurtebise: the guess was pretty well-founded, as the last two digits of every track in this box set was equal to the track number … except for this duplicate.
Looking up HKI190057913 on the ifpi site (thanks ListMyCDs.com for the link!) proofs that it was the intended ISRC for this recording.
I still have the nagging question whether it is more likely that my individual copy (or drive) contains the wrong ISRC (small errors occur) … or that an error happened during production, which resulted in all copies sporting this particular mistake.
If the latter, maybe it would be better to leave the wrong ISRC on the recording?