diff -r 60dbf0b3f6c7 -r af73cf0dc31f doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Sep 01 23:43:45 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Sep 02 00:48:07 2010 +0200
@@ -108,7 +108,7 @@
     @{index_ML Proof.show_main_goal: "bool Unsynchronized.ref"} & default @{ML false} \\
     @{index_ML show_hyps: "bool Unsynchronized.ref"} & default @{ML false} \\
     @{index_ML show_tags: "bool Unsynchronized.ref"} & default @{ML false} \\
-    @{index_ML show_question_marks: "bool Unsynchronized.ref"} & default @{ML true} \\
+    @{index_ML show_question_marks: "bool Config.T"} & default @{ML true} \\
   \end{mldecls}
 
   These global ML variables control the detail of information that is