translator now proves check_ctors_decs
got HOL light example running again -- was out of date