Re: [GiNaC-list] set_TeX_name() ?