reveal

Parse.reveal : string -> unit

Restores recognition of a constant by the quotation parser.

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.

See also

Parse.hide, Parse.hidden, Parse.remove_ovl_mapping, Parse.update_overload_maps