--- a/doc-src/IsarImplementation/Thy/ML.thy Fri Oct 08 21:49:16 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy Sat Oct 09 19:05:31 2010 +0100
@@ -204,7 +204,7 @@
perspective on Isabelle/ML antiquotations.
*}
-text %mlref {*
+text %mlantiq {*
\begin{matharray}{rcl}
@{ML_antiquotation_def "let"} & : & @{text ML_antiquotation} \\
@{ML_antiquotation_def "note"} & : & @{text ML_antiquotation} \\
--- a/doc-src/IsarImplementation/style.sty Fri Oct 08 21:49:16 2010 +0100
+++ b/doc-src/IsarImplementation/style.sty Sat Oct 09 19:05:31 2010 +0100
@@ -25,9 +25,14 @@
\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
\isafoldtag{FIXME}
+
\isakeeptag{mlref}
-\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Reference}\begingroup\def\isastyletext{\rm}}
-\renewcommand{\endisatagmlref}{\endgroup}
+\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Reference}}
+\renewcommand{\endisatagmlref}{}
+
+\isakeeptag{mlantiq}
+\renewcommand{\isatagmlantiq}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Antiquotations}}
+\renewcommand{\endisatagmlantiq}{}
\isakeeptag{mlex}
\renewcommand{\isatagmlex}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Examples}}