diff -r f03ec7fae947 -r 7c2b13a53d69 src/Doc/IsarImplementation/ML.thy
--- a/src/Doc/IsarImplementation/ML.thy	Fri Aug 23 11:44:28 2013 +0200
+++ b/src/Doc/IsarImplementation/ML.thy	Fri Aug 23 12:30:51 2013 +0200
@@ -682,61 +682,6 @@
   scheme allows to refer to formal entities in a robust manner, with
   proper static scoping and with some degree of logical checking of
   small portions of the code.
-
-  Special antiquotations like @{text "@{let \<dots>}"} or @{text "@{note
-  \<dots>}"} augment the compilation context without generating code.  The
-  non-ASCII braces @{text "\<lbrace>"} and @{text "\<rbrace>"} allow to delimit the
-  effect by introducing local blocks within the pre-compilation
-  environment.
-
-  \medskip See also \cite{Wenzel-Chaieb:2007b} for a broader
-  perspective on Isabelle/ML antiquotations.  *}
-
-text %mlantiq {*
-  \begin{matharray}{rcl}
-  @{ML_antiquotation_def "let"} & : & @{text ML_antiquotation} \\
-  @{ML_antiquotation_def "note"} & : & @{text ML_antiquotation} \\
-  \end{matharray}
-
-  @{rail "
-  @@{ML_antiquotation let} ((term + @'and') '=' term + @'and')
-  ;
-  @@{ML_antiquotation note} (thmdef? thmrefs + @'and')
-  "}
-
-  \begin{description}
-
-  \item @{text "@{let p = t}"} binds schematic variables in the
-  pattern @{text "p"} by higher-order matching against the term @{text
-  "t"}.  This is analogous to the regular @{command_ref let} command
-  in the Isar proof language.  The pre-compilation environment is
-  augmented by auxiliary term bindings, without emitting ML source.
-
-  \item @{text "@{note a = b\<^sub>1 \<dots> b\<^sub>n}"} recalls existing facts @{text
-  "b\<^sub>1, \<dots>, b\<^sub>n"}, binding the result as @{text a}.  This is analogous to
-  the regular @{command_ref note} command in the Isar proof language.
-  The pre-compilation environment is augmented by auxiliary fact
-  bindings, without emitting ML source.
-
-  \end{description}
-*}
-
-text %mlex {* The following artificial example gives some impression
-  about the antiquotation elements introduced so far, together with
-  the important @{text "@{thm}"} antiquotation defined later.
-*}
-
-ML {*
-  \<lbrace>
-    @{let ?t = my_term}
-    @{note my_refl = reflexive [of ?t]}
-    fun foo th = Thm.transitive th @{thm my_refl}
-  \<rbrace>
-*}
-
-text {* The extra block delimiters do not affect the compiled code
-  itself, i.e.\ function @{ML foo} is available in the present context
-  of this paragraph.
 *}