Aha, it's merely a different file these days. The file you listed was from an old version. What we're looking for here is this file:

/Applications/Arduino.app/Contents/Java/hardware/arduino/avr/cores/arduino/HardwareSerial.h

That one hits the #error statement if I insert it, and also, it has separate RX and TX buffers.

Now we're talkin'.