string_append().  These must be artifacts of GvR's rewrite.

Fixed some typos in the leading comment (and re-filled the
paragraphs).

Hope you don't mind, Guido.