Expansion of double backticks and commas

I see that SBCL expands this way:

``(,,@'(0 1 2) ,3) -> `(,0 ,1 ,2 ,3)

so apparently the second comma is consumed while the first one is copied before each element of the spliced list.

This behavior seems peculiar to sbcl, as clisp evaluates that form to (LIST* 0 1 2 '(3)) and gcl to (LIST 0 1 2 3): they both discard the other backtick-comma pair.

I wonder what ANSI says on the matter. Does any of the two behaviors, the sbcl's and the clisp/gcl's, follows from the basic rules, for example those in http://www.lispworks.com/documentation/HyperSpec/Body/02_df.htm?

I'd appreciate any help. Thanks,

Andrea Monaco