This reverts commit 2065317d.

I committed a wrong version of this patch.
Also reverts the follow-up commits 77a3dfb3 and 8331e591.