diff -r 8537313dd261 -r 55c305e29f4b doc-src/IsarImplementation/Thy/Syntax.thy
--- a/doc-src/IsarImplementation/Thy/Syntax.thy	Wed Jun 20 20:50:04 2012 +0200
+++ b/doc-src/IsarImplementation/Thy/Syntax.thy	Wed Jun 20 21:18:35 2012 +0200
@@ -160,31 +160,4 @@
   \end{description}
 *}
 
-
-section {* Syntax translations *}
-
-text FIXME
-
-text %mlantiq {*
-  \begin{matharray}{rcl}
-  @{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}
-
-  @{rail "
-  (@@{ML_antiquotation class_syntax} |
-   @@{ML_antiquotation type_syntax} |
-   @@{ML_antiquotation const_syntax} |
-   @@{ML_antiquotation syntax_const}) name
-  "}
-
-  \begin{description}
-
-  \item FIXME
-
-  \end{description}
-*}
-
 end