unhide_constant : string -> unit
Restores recognition of a constant by the quotation parser.
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
- FAILURE CONDITIONS
Fails unless the given name is a hidden constant in the current theory.
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