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.