Final polish concerning #543

Hmm.  I would slightly prefer if `Empty_rec` were defined in terms of `Empty_ind`, the way we do it for HITs.