# HG changeset patch
# User wenzelm
# Date 1286647531 -3600
# Node ID 7c501d7f1e45546e4dd1375af331cc905e636328
# Parent  f5ea50decd9f92973da01a3dcae602d03addd5c0
clarified tag markup;

diff -r f5ea50decd9f -r 7c501d7f1e45 doc-src/IsarImplementation/Thy/ML.thy
--- 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} \\
diff -r f5ea50decd9f -r 7c501d7f1e45 doc-src/IsarImplementation/style.sty
--- 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}}