diff -r 3305f573294e -r b47d41d9f4b5 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat Apr 16 12:46:18 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat Apr 16 13:48:45 2011 +0200
@@ -122,10 +122,10 @@
     \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}{show\_abbrevs}\verb|show_abbrevs: bool Config.T| & default \verb|true| \\
-    \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| \\
-    \indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\
     \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Config.T| & default \verb|false| \\
+    \indexdef{}{ML}{Name\_Space.long\_names}\verb|Name_Space.long_names: bool Config.T| & default \verb|false| \\
+    \indexdef{}{ML}{Name\_Space.short\_names}\verb|Name_Space.short_names: bool Config.T| & default \verb|false| \\
+    \indexdef{}{ML}{Name\_Space.unique\_names}\verb|Name_Space.unique_names: bool Config.T| & default \verb|true| \\
     \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| \\
@@ -165,11 +165,6 @@
 
   \item \verb|show_abbrevs| controls folding of constant abbreviations.
 
-  \item \verb|long_names|, \verb|short_names|, and \verb|unique_names|
-  control the way of printing fully qualified internal names in
-  external form.  See also \secref{sec:antiq} for the document
-  antiquotation options of the same names.
-
   \item \verb|show_brackets| controls bracketing in pretty printed
   output.  If set to \verb|true|, all sub-expressions of the pretty
   printing tree will be parenthesized, even if this produces malformed
@@ -177,6 +172,12 @@
   pretty printed entities may occasionally help to diagnose problems
   with operator priorities, for example.
 
+  \item \verb|Name_Space.long_names|, \verb|Name_Space.short_names|, and
+  \verb|Name_Space.unique_names| control the way of printing fully
+  qualified internal names in external form.  See also
+  \secref{sec:antiq} for the document antiquotation options of the
+  same names.
+
   \item \verb|eta_contract| controls \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-contracted printing of
   terms.