Removed push_enable and pop_enable. They are not used.
We may want *something* like this later, as cyrille just
proposed, but probably not in this form.