(redefined-names state) returns nil then no unsafe
definitions have been made, regardless of ld-redefinition-action.
See ld-redefinition-action.
Major Section: MISCELLANEOUS
Example and General Forms: (redefined-names state)
This function collects names that have been redefined in the current ACL2
state. :Program mode functions that were reclassified to
:logic functions are not collected, since such reclassification
cannot imperil soundness because it is allowed only when the new and old
definitions are identical.
Thus, if (redefined-names state) returns nil then no unsafe
definitions have been made, regardless of ld-redefinition-action.
See ld-redefinition-action.