the non-normalized definition
of a function,
ensuring that the name of the theorem will not cause a conflict.
This utility is an event which, when evaluated successfully, installs the
event generated by install-not-normalized-event. See install-not-normalized-event.
This is related to install-not-normalized.
(defmacro install-not-normalized$ (fn &key allp names-to-avoid)
(cons (cons 'install-not-normalized$-fn
(cons (cons 'quote (cons fn 'nil))
(cons allp (cons names-to-avoid '(state)))))