Haha, that would be correct! Thanks, Brian. I added the following after line 106 of pins_teensy.c (still just working with these three pins):
{GPIO_BITBAND_PTR(CORE_PIN72_PORTREG, CORE_PIN72_BIT), &CORE_PIN72_CONFIG}, // new
{GPIO_BITBAND_PTR(CORE_PIN73_PORTREG, CORE_PIN73_BIT)...