I see nothing bad in the idea of partially superposing two plus signs. I've never seen such notation before, but it's not difficult to do it right, which is not the case with the macro you found out.
\documentclass{article}
\usepackage{amsmath}
\newcommand{\concat}{%
\mathbin{{+}\mspace{-8mu}{+}}%
}
\newcommand{\starop}[1]{\mathop{#1^*}}
\begin{document}
\begin{gather*}
({\concat}): \forall X.\ X^* \to X^* \to X^* \\
\starop{a}(xs\concat_{A} ys)=(\starop{a} xs)\concat_{A'}(\starop{a} ys)
\end{gather*}
\end{document}

Compare with the original:

They seem to differ only for better spacing in my output. ;-)
Maybe the distance between the vertical bars is slightly different, adjust it to suit.
And yes, the original uses two plus signs, judging from the DVI file that I transformed into PDF.
Alternative version
You might prefer a different symbol, as high and wide as the standard plus sign.
The use of color is to show precisely that the two symbols have the same width (red or black never overspills). Again, adjust the distance between the vertical bars to suit.
\documentclass{article}
\usepackage{amsmath,pict2e,color}
\makeatletter
\newcommand{\concat}{\mathbin{\mathpalette\conc@t\relax}}
\newcommand{\conc@t}[2]{%
\vcenter{\hbox{%
\sbox\z@{$\m@th#1-$}%
\setlength{\unitlength}{\wd\z@}%
\begin{picture}(1,1)
\roundcap
\put(0.1,0.5){\line(1,0){0.8}}
\put(0.35,0.1){\line(0,1){0.8}}
\put(0.65,0.1){\line(0,1){0.8}}
\end{picture}%
}}%
}
\makeatother
\newcommand{\starop}[1]{\mathop{#1^*}}
\begin{document}
\begin{gather*}
\rlap{\color{red}$+$}{\concat}{\concat}\llap{\color{red}$+$}\\
\rlap{\color{red}$\concat$}{+}{+}\llap{\color{red}$\concat$}\\
{+}{\concat}\quad a_{\concat_{\concat}}\\
{+}\\
{\concat}\\
({\concat}): \forall X.\ X^* \to X^* \to X^* \\
\starop{a}(xs\concat_{A} ys)=(\starop{a} xs)\concat_{A'}(\starop{a} ys)
\end{gather*}
\end{document}

;-)
\mathbin
, why didn't use that in your\concat
command?