There was a stray factor of 2 (VBAT_DIV) that looks like it was copied incorrectly from the read_core_vbat() function.
The factor exists in read_core_vbat() because VBAT is measured through a 2:1 voltage divider.
read_core_vref now returns values around 1.21V (assuming that external reference voltage is 3.3V) which is in line with the datasheet values.
See comment at http://forum.micropython.org/viewtopic.php?f=6&t=533&p=2991#p2991