Fix code for handling sign extension of negative 12-bit values.
Previous code was incorrect; this code is also faster and simpler