Agda now reduces types before checking that they are data types

This was a super silly mistake I made in my hack for solving Issue 1023 (https://code.google.com/p/agda/issues/detail?id=1023), which caused the termination checker to complain a LOT more than necessary when --without-K was enabled (see also https://code.google.com/p/agda/issues/detail?id=1214). If possible, please check that there are no other obvious mistakes (it's only a few lines).