unhide_constant : string -> unit

SYNOPSIS
Restores recognition of a constant by the quotation parser.

DESCRIPTION
A call unhide_constant "c", where c is a hidden constant, will unhide the constant, that is, will make the quotation parser recognize it as such rather than parsing it as a variable. It reverses the effect of the call hide_constant name.

FAILURE CONDITIONS
Fails unless the given name is a hidden constant in the current theory.

COMMENTS
The hiding of a constant only affects the quotation parser; the constant is still there in a theory, and may not be redefined.

SEE ALSO
hide_constant, is_hidden.