Thanks for the pointer. I ended up finding the font files in /usr/share/mplayer rather than /usr/share/local/mplayer, where I'd expected. Just swap the size you want into the ~/font directory. Problem solved. Thanks again.