change an ordinary macro command to an atomic macro, or vice-versa
Major Section:  PROOF-CHECKER

(toggle-pc-macro pro)
Change pro from an atomic macro command to an ordinary one (or vice-versa, if pro happens to be an ordinary macro command)

General Form:
(toggle-pc-macro name &optional new-tp)
If name is an atomic macro command then this turns it into an ordinary one, and vice-versa. However, if new-tp is supplied and not nil, then it should be the new type (the symbol macro or atomic-macro, in any package), or else there is no change.