diff -r 245b64afefe2 -r ef2a7b589004 doc-src/Ref/syntax.tex
--- a/doc-src/Ref/syntax.tex	Fri Dec 05 18:44:56 1997 +0100
+++ b/doc-src/Ref/syntax.tex	Fri Dec 05 18:45:19 1997 +0100
@@ -715,12 +715,13 @@
 {\tt print_syntax} displays the sets of names associated with the
 translation functions of a theory under
 \ttindex{parse_ast_translation}, \ttindex{parse_translation},
-\ttindex{print_translation} and \ttindex{print_ast_translation}.  You
-can add new ones via the {\tt ML} section\index{*ML section} of a
-theory definition file.  There may never be more than one function of
-the same kind per name.  Even though the {\tt ML} section is the very
-last part of the file, newly installed translation functions are
-already effective when processing all of the preceding sections.
+\ttindex{print_translation} (or \ttindex{typed_print_translation}) and
+\ttindex{print_ast_translation}.  You can add new ones via the {\tt
+  ML} section\index{*ML section} of a theory definition file.  There
+may never be more than one function of the same kind per name.  Even
+though the {\tt ML} section is the very last part of the file, newly
+installed translation functions are already effective when processing
+all of the preceding sections.
 
 The {\tt ML} section's contents are simply copied verbatim near the
 beginning of the \ML\ file generated from a theory definition file.
@@ -733,7 +734,8 @@
 val print_ast_translation   : (string * (ast list -> ast)) list
 val parse_translation       : (string * (term list -> term)) list
 val print_translation       : (string * (term list -> term)) list
-val typed_print_translation : (string * (typ -> term list -> term)) list
+val typed_print_translation :
+    (string * (bool -> typ -> term list -> term)) list
 \end{ttbox}
 
 \subsection{The translation strategy}
@@ -751,7 +753,8 @@
 (c, \tau) \ttapp x@1 \ttapp \ldots \ttapp x@n$.  Terms allow more
 sophisticated transformations than \AST{}s do, typically involving
 abstractions and bound variables. {\em Typed} print translations may
-even peek at the type $\tau$ of the constant they are invoked on.
+even peek at the type $\tau$ of the constant they are invoked on; they
+are also passed the current value of the \ttindex{show_sorts} flag.
 
 Regardless of whether they act on terms or \AST{}s, translation
 functions called during the parsing process differ from those for