defthm-support-for-on-failure-local

(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 '(:or (with-output :stack :pop ,NEW-FORM)
              (encapsulate nil
                (local (include-book "acl2s/cgen/top" :dir :system :ttags :all))
                (local (acl2s-defaults :set testing-enabled t))
                (with-output :stack :pop ,NEW-FORM)
                (mv nil nil state)))
            :expansion? ,NEW-FORM))))))