I think there may be an inaccuracy in the specification, which states that
marks are applied to introduced identifiers in the output of the transformer
(as opposed to the output of a SYNTAX expression).  If this were accurate, I
believe the following should print #t.  Instead, it prints #f.

(define-syntax test
   (syntax-rules ()
     ((_ id)
      (let-syntax ((foo (lambda (s)
                          (syntax-case s ()
                            ((_ id*)
                             (begin
                               (display (bound-identifier=?
                                         (syntax id)
                                         (syntax id*)))
                               (syntax 'done)))))))
        (foo id)))))

(test x)

It would print #t because (syntax id) has not yet been output by the inner
transformer (and indeed will never be), and therefore it has not yet been
marked.

If I use the antimark prescription to follow what happens, and compare
identifiers using both marks and antimarks, I indeed get the correct result #f.
However, the text of the SRFI does not describe antimarks as essential to the
semantics, but rather as an implementation strategy.

Regards
Andre