xdoc error on encapsulated DEFINE with local other-events and :progn t

[kini]

This was initially reported by @acoglio on the acl2-help mailing list as an issue with xdoc and an FTY deftagsum with only one summand. I reduced the repro case to the following:

(include-book "std/util/define" :dir :system)
(encapsulate ()
  (define foo (x) x
    :short "" :progn t
    /// (local (defthm bar (equal (foo (foo x)) x)))))
:doc foo

Output from the :doc command:

[...]
; xdoc error in FOO: get-event failed for BAR.
ACL2::FOO -- Current Interactive Session

    Signature

        (foo x) --> *


Definitions and Theorems

  Function: <foo>

    (defun foo (x)
           (declare (xargs :guard t))
           (let ((__function__ 'foo))
                (declare (ignorable __function__))
                x))

  Definition: <bar>

    "Error getting event for ACL2::BAR"