----------------------------------------------------------------------
disable_tyabbrev_printing                                      (Parse)
----------------------------------------------------------------------
disable_tyabbrev_printing : string -> unit

SYNOPSIS
Disables the printing of a type abbreviation.

KEYWORDS
Pretty-printing

DESCRIBE
A call to {disable_tyabbrev_printing s} causes type abbreviations
mapping the string {s} to some type expansion not to be printed when
an instance of the type expansion is seen.

If the string {s} is not a qualified name (of the form {"thy$name"}),
then all type abbreviations with base name {s} are disabled. If {s}
does have a qualified name, then only a type abbreviation of that name
and theory will be disabled (if such exists).

FAILURE
Fails if the given string is a malformed qualified identifier (e.g.,
{foo$$}). If the given name is syntactically valid, but there are no
abbreviations keyed to the given name, a call to
{disable_tyabbrev_printing} will silently do nothing.

EXAMPLE

- type_abbrev("LIST", ``:'a list``)
> val it = () : unit

- ``:num list``;
> val it = ``:num LIST`` : hol_type

- disable_tyabbrev_printing "LIST";
> val it = () : unit

- ``:num LIST``;
> val it = ``:num list`` : hol_type


COMMENTS
When a type-abbreviation is established with the function
{type_abbrev}, this alters both parsing and printing: when the new
abbreviation appears in input the type parser will translate away the
abbreviation.  Similarly, when an instance of the abbreviation appears
in a type that the printer is to output, it will replace the instance
with the abbreviation.

This is generally the appropriate behaviour.  However, there is are a
number of useful abbreviations where reversing parsing when printing
is not so useful.  For example, the abbreviation mapping {'a set} to
{'a -> bool} is convenient, but it would be a mistake having it print
because types such as that of conjunction would print as

   (/\) : bool -> bool set

which is rather confusing.

As with other printing and parsing functions, there is a version of
this function, {temp_disable_tyabbrev_printing} that does not cause
its effect to persist with an exported theory.

SEEALSO
Parse.remove_type_abbrev, Parse.type_abbrev.

----------------------------------------------------------------------