Remove unused file.

This was added in 10540974, but has
never been used for anything as far as I can tell.  There seems to
be no reason to keep it.