# HG changeset patch
# User wenzelm
# Date 1286568716 -3600
# Node ID 4303afd3612ad70c1007a1c925b0dbb5e3ddd150
# Parent  d829ce302ca4bfd687b2b344c60e27051047338b
keep normal size for %mlref tag;

diff -r d829ce302ca4 -r 4303afd3612a doc-src/IsarImplementation/style.sty
--- a/doc-src/IsarImplementation/style.sty	Fri Oct 08 20:59:01 2010 +0100
+++ b/doc-src/IsarImplementation/style.sty	Fri Oct 08 21:11:56 2010 +0100
@@ -26,7 +26,7 @@
 
 \isafoldtag{FIXME}
 \isakeeptag{mlref}
-\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
+\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Reference}\begingroup\def\isastyletext{\rm}}
 \renewcommand{\endisatagmlref}{\endgroup}
 
 \isakeeptag{mlex}