Fix copy-paste mistaked pointed out by Thomas Munro