Redex: remove some now extraneous code