On Sat, 26 Jan 2008, Steven Obua wrote: > Makarius wrote: > > >This is because token translations are only used when printing terms, not > >when presenting theory sources. > > > Yes, I noticed that. > > Is there any quick hack around it ? No way. Makarius