		Search-engine friendly clone of the ACL2 documentation.

Macros

Remove-macro-alias

Remove the association of a function name with a macro name

Example:
(remove-macro-alias append)

General Form:
(remove-macro-alias macro-name)

See macro-aliases-table for a discussion of macro aliases; also see add-macro-alias. This form sets macro-aliases-table to the result of deleting the key macro-name from that table. If the name does not occur in the table, then this form still generates an event, but the event has no real effect.