--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sun Sep 05 19:47:40 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sun Sep 05 21:41:24 2010 +0200
@@ -118,8 +118,8 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML}{show\_types}\verb|show_types: bool Unsynchronized.ref| & default \verb|false| \\
- \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Unsynchronized.ref| & default \verb|false| \\
+ \indexdef{}{ML}{show\_types}\verb|show_types: bool Config.T| & default \verb|false| \\
+ \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Config.T| & default \verb|false| \\
\indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\
\indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\
\indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\