- STRUCTURE
- SYNOPSIS
Restores recognition of a constant by the quotation parser.
- LIBRARY
Parse
- DESCRIPTION
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