[isabelle-dev] token translations

[Steven Obua]

Hi,

I am using the Isar token translation mechanism to modify the latex 
generation of Isabelle.

token_translation {*
 .....
*}

This works fine if if output stuff for example like that

text{*
   @{thm float_add}
*}

But it does not work for the main output of a theory, like

lemma "balabla"
sorry

The token translations are not applied to "balabla". How can I fix this ?

Steven