terminal @number vs. @user-number

[Joel E. Denny]

Currently, Bison puts a terminal's user number (the one returned by yylex) 
in its XML "number" attribute.  I think we should rename that to 
"user-number" and add a "number" attribute for Bison's internal symbol 
number.  This would be more consistent with nonterminals.  I'd be happy 
the write the patch.  Is all this agreeable to you, Wojciech?