Revert "More work on #827: removed now-unneeded code"

This reverts commit 8d2c7cba23390421afe051373efde220da46503c.