reveal : string -> unit
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
HOL  Trindemossen-1