defthm-support-for-on-failure

(defmacro defthm
  (&whole event-form
    name
    term
    &key
    (rule-classes '(:rewrite))
    instructions
    hints
    otf-flg
    (no-retry 'nil))
  (cond (no-retry `(defthm-fn ',NAME
        ',TERM
        state
        ',RULE-CLASSES
        ',INSTRUCTIONS
        ',HINTS
        ',OTF-FLG
        ',EVENT-FORM))
    (t (let ((new-form `(defthm ,NAME
             ,TERM
             :no-retry t
             ,@(REMOVE-KEYWORD :NO-RETRY (CDDDR EVENT-FORM)))))
        `(with-output :off :all :stack :push (make-event (b* ((testing? (acl2s-defaults :get testing-enabled)))
              (if (eq testing? :on-failure)
                '(:or (encapsulate nil
                    (local (acl2s-defaults :set testing-enabled nil))
                    (with-output :stack :pop ,NEW-FORM))
                  (with-output :stack :pop ,NEW-FORM))
                '(with-output :stack :pop ,NEW-FORM)))
            :expansion? ,NEW-FORM))))))