diff -r 348aed032cda -r 36ffe23b25f8 src/Doc/IsarRef/Inner_Syntax.thy
--- a/src/Doc/IsarRef/Inner_Syntax.thy	Sat May 25 15:00:53 2013 +0200
+++ b/src/Doc/IsarRef/Inner_Syntax.thy	Sat May 25 15:37:53 2013 +0200
@@ -1469,7 +1469,7 @@
   @{rail "
   ( @@{command parse_ast_translation} | @@{command parse_translation} |
     @@{command print_translation} | @@{command typed_print_translation} |
-    @@{command print_ast_translation}) ('(' @'advanced' ')')? @{syntax text}
+    @@{command print_ast_translation}) @{syntax text}
   ;
   (@@{ML_antiquotation class_syntax} |
    @@{ML_antiquotation type_syntax} |
@@ -1486,31 +1486,31 @@
 
   \medskip
   {\footnotesize
-  \begin{tabular}{ll}
-  @{command parse_ast_translation} & : @{ML_type "(string * (Ast.ast list -> Ast.ast)) list"} \\
-  @{command parse_translation} & : @{ML_type "(string * (term list -> term)) list"} \\
-  @{command print_translation} & : @{ML_type "(string * (term list -> term)) list"} \\
-  @{command typed_print_translation} & : @{ML_type "(string * (typ -> term list -> term)) list"} \\
-  @{command print_ast_translation} & : @{ML_type "(string * (Ast.ast list -> Ast.ast)) list"} \\
+  \begin{tabular}{l}
+  @{command parse_ast_translation} : \\
+  \quad @{ML_type "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"} \\
+  @{command parse_translation} : \\
+  \quad @{ML_type "(string * (Proof.context -> term list -> term)) list"} \\
+  @{command print_translation} : \\
+  \quad @{ML_type "(string * (Proof.context -> term list -> term)) list"} \\
+  @{command typed_print_translation} : \\
+  \quad @{ML_type "(string * (Proof.context -> typ -> term list -> term)) list"} \\
+  @{command print_ast_translation} : \\
+  \quad @{ML_type "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"} \\
   \end{tabular}}
   \medskip
 
   The argument list consists of @{text "(c, tr)"} pairs, where @{text
   "c"} is the syntax name of the formal entity involved, and @{text
   "tr"} a function that translates a syntax form @{text "c args"} into
-  @{text "tr args"}.  The ML naming convention for parse translations
-  is @{text "c_tr"} and for print translations @{text "c_tr'"}.
+  @{text "tr ctxt args"} (depending on the context).  The ML naming
+  convention for parse translations is @{text "c_tr"} and for print
+  translations @{text "c_tr'"}.
 
   The @{command_ref print_syntax} command displays the sets of names
   associated with the translation functions of a theory under @{text
   "parse_ast_translation"} etc.
 
-  If the @{verbatim "("}@{keyword "advanced"}@{verbatim ")"} option is
-  given, the corresponding translation functions depend on the current
-  theory or proof context as additional argument.  This allows to
-  implement advanced syntax mechanisms, as translations functions may
-  refer to specific theory declarations or auxiliary proof data.
-
   \item @{text "@{class_syntax c}"}, @{text "@{type_syntax c}"},
   @{text "@{const_syntax c}"} inline the authentic syntax name of the
   given formal entities into the ML source.  This is the