doc-src/IsarRef/Thy/document/Inner_Syntax.tex

   translation functions may depend on the current theory or proof
   context.  This allows to implement advanced syntax mechanisms, as
   translations functions may refer to specific theory declarations or
   auxiliary proof data.
 
-  See also \cite{isabelle-ref} for more information on the general
-  concept of syntax transformations in Isabelle.
-
 %FIXME proper antiquotations
 \begin{ttbox}
 val parse_ast_translation:
   (string * (Proof.context -> ast list -> ast)) list
 val parse_translation:

   (string * (Proof.context -> term list -> term)) list
 val typed_print_translation:
   (string * (Proof.context -> typ -> term list -> term)) list
 val print_ast_translation:
   (string * (Proof.context -> ast list -> ast)) list
-\end{ttbox}%
+\end{ttbox}
+
+  \medskip See also the chapter on ``Syntax Transformations'' in old
+  \cite{isabelle-ref} for further details on translations on parse
+  trees.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isadelimtheory
 %