diff -r 60dbf0b3f6c7 -r af73cf0dc31f doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Sep 01 23:43:45 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Sep 02 00:48:07 2010 +0200
@@ -130,7 +130,7 @@
     \indexdef{}{ML}{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool Unsynchronized.ref| & default \verb|false| \\
     \indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool Unsynchronized.ref| & default \verb|false| \\
     \indexdef{}{ML}{show\_tags}\verb|show_tags: bool Unsynchronized.ref| & default \verb|false| \\
-    \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Unsynchronized.ref| & default \verb|true| \\
+    \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Config.T| & default \verb|true| \\
   \end{mldecls}
 
   These global ML variables control the detail of information that is