remove_user_printer :
  string -> (term * term_grammar.userprinter) option
STRUCTURE
SYNOPSIS
Removes a user-defined pretty-printing function associated with a particular name.
LIBRARY
Parse
DESCRIPTION
This removes the user-defined pretty-printing function that has been associated with a particular name (the name of the code for the function). If there is such a printer in the global grammar for the specified type, this is returned in the option type. If there is no printer, then NONE is returned.
FAILURE
Never fails.
COMMENTS
As always, there is an accompanying function temp_remove_user_printer, which does not affect the grammar exported to disk.
SEEALSO
HOL  Kananaskis-14