hide_constant : string -> unit

SYNOPSIS
Stops the quotation parser from recognizing a constant.

DESCRIPTION
A call hide_constant "c" where c is the name of a constant, will prevent the quotation parser from parsing it as such; it will just be parsed as a variable. The effect can be reversed by unhide_constant "c".

FAILURE CONDITIONS
Fails if the given name is not a constant of the current theory, or if the named constant is already hidden.

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
unhide_constant.