This patch which /improves/ status quo. Applies cleanly on top of
earlier patch at http://debbugs.gnu.org/cgi/bugreport.cgi?bug=11095#94

This patch makes sure that faces used for highlighting are always
distinct and recycles them only when it is inevitable.