Remove user-defined color printer from the HOL Light term printing.
DESCRIPTION
HOL Light allows arbitrary user printers to be inserted into the toplevel
printer so that they are invoked on all applicable subterms (see
install_user_printer and install_user_color_printer).
The call delete_user_color_printer s removes any such printer
associated with the tag s that is registered by install_user_color_printer.
FAILURE CONDITIONS
Never fails, even if there is no printer with the given tag.