On Mon, 26 Jan 2015, Florian Haftmann wrote: > I think it is best if I find a possibility to print strings in a way > that is both digestible for Isabelle/ML and (S)ML. If it is just for generated sources, you could use "\092" for backslash and thus escape further special treatment as Isabelle symbols. Makarius