--- 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.
*}