
diff -r cc7abfe6d5e7 -r 878d86983dc1 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Sep 10 15:36:49 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Sep 10 15:38:54 2010 +0200
@@ -128,8 +128,8 @@
     \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool Config.T| & default \verb|true| \\
     \indexdef{}{ML}{Goal\_Display.goals\_limit}\verb|Goal_Display.goals_limit: int Config.T| & default \verb|10| \\
     \indexdef{}{ML}{Goal\_Display.show\_main\_goal}\verb|Goal_Display.show_main_goal: bool Config.T| & 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\_hyps}\verb|show_hyps: bool Config.T| & default \verb|false| \\
+    \indexdef{}{ML}{show\_tags}\verb|show_tags: bool Config.T| & default \verb|false| \\
     \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Config.T| & default \verb|true| \\
   \end{mldecls}
 




