# HG changeset patch
# User wenzelm
# Date 1395086081 -3600
# Node ID 01fb1b35433b4f74f8da68c5d6cb33a4532c473a
# Parent  851c7b05eb92e1ee313fe2133db5e67a7242757f
tuned;

diff -r 851c7b05eb92 -r 01fb1b35433b src/Doc/IsarRef/Inner_Syntax.thy
--- a/src/Doc/IsarRef/Inner_Syntax.thy	Mon Mar 17 20:48:58 2014 +0100
+++ b/src/Doc/IsarRef/Inner_Syntax.thy	Mon Mar 17 20:54:41 2014 +0100
@@ -1453,10 +1453,10 @@
     @{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{ML_antiquotation_def "class_syntax"} & : & @{text ML_antiquotation} \\
-    @{ML_antiquotation_def "type_syntax"} & : & @{text ML_antiquotation} \\
-    @{ML_antiquotation_def "const_syntax"} & : & @{text ML_antiquotation} \\
-    @{ML_antiquotation_def "syntax_const"} & : & @{text ML_antiquotation} \\
+    @{ML_antiquotation_def "class_syntax"} & : & @{text "ML antiquotation"} \\
+    @{ML_antiquotation_def "type_syntax"} & : & @{text "ML antiquotation"} \\
+    @{ML_antiquotation_def "const_syntax"} & : & @{text "ML antiquotation"} \\
+    @{ML_antiquotation_def "syntax_const"} & : & @{text "ML antiquotation"} \\
   \end{matharray}
 
   Syntax translation functions written in ML admit almost arbitrary