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 ? Steven