diff -r b98f22593f97 -r 04dfffda5671 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue May 03 22:26:16 2011 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue May 03 22:27:32 2011 +0200
@@ -152,7 +152,7 @@
 the qualified name, for example @{text "T.length"}, where @{text T} is the
 theory it is defined in, to distinguish it from the predefined @{const[source]
 "List.length"}. In case there is no danger of confusion, you can insist on
-short names (no qualifiers) by setting the \verb!short_names!
+short names (no qualifiers) by setting the \verb!names_short!
 configuration option in the context.
 *}