Thanks very much to Prof Brian Ripley <ripley at stats.ox.ac.uk> for the quick and illuminating reply:
We have corrected a bug: you now get the size you ask for... DId you think to actually measure the sizes? Might be interesting (although you may need to measure the window too).
Sticking a ruler up to my screen, I measure the "12pt" font at 13.5 pt (where 1 pt = 1/72 inch), and the "10pt" at 9.5 pt. My window as a whole is about 1.2x as large as I asked for, though. So the "10pt" font is a little small, but the sizes are roughly right (in R-2.1.0). -- David Brahm (brahm at alum.mit.edu)