Pretty: kill code that has been dead since 1997 (#10735)