----------------------------------------------------------------------
show_types                                                   (Globals)
----------------------------------------------------------------------
Globals.show_types : bool ref

SYNOPSIS
Flag controlling printing of HOL types (in terms).

DESCRIBE
Normally HOL types in terms are not printed, since this makes terms
hard to read. Type printing is enabled by {show_types := true}, and
disabled by {show_types := false}. When printing of types is enabled, not
all variables and constants are annotated with a type. The intention
is to provide sufficient type information to remove any ambiguities
without swamping the term with type information.

FAILURE
Never fails.

EXAMPLE

- BOOL_CASES_AX;;
> val it = |- !t. (t = T) \/ (t = F) : thm

- show_types := true;
> val it = () : unit

- BOOL_CASES_AX;;
> val it = |- !(t :bool). (t = T) \/ (t = F) : thm




COMMENTS
It is possible to construct an abstraction in which the bound variable
has the same name but a different type to a variable in the body. In
such a case the two variables are considered to be distinct. Without
type information such a term can be very misleading, so it might be a
good idea to provide type information for the free variable whether or
not printing of types is enabled.

SEEALSO
Parse.print_term.

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