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

SYNOPSIS
Restores recognition of a constant by the quotation parser.

LIBRARY
Parse

DESCRIBE
A call {reveal c}, where {c} the name of a (perhaps) hidden constant,
will ‘unhide’ the constant, that is, will make the quotation parser map
the identifier {c} to all current constants with the same name (there may
be more than one such as different theories may re-use the same name).

FAILURE
Never fails, but prints a warning message if the string does not
correspond to an actual constant.

COMMENTS
The hiding of a constant only affects the quotation parser;
the constant is still there in a theory.  If the parameter {c} is
already overloaded so as to map to other constants, these overloadings
are not altered.

SEEALSO
Parse.hide, Parse.hidden, Parse.remove_ovl_mapping,
Parse.update_overload_maps.

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