That code wasn't about something you'd need to do. That was me trying to figure out how the thing worked. If you keep going on that thread you get to this post which is the end of the story there.
But again, you don't need this. The Arduino core already has functions to attach the ADC interrupts.