--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu Aug 30 22:35:40 2007 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Aug 31 12:24:00 2007 +0200
@@ -133,6 +133,19 @@
(*<*)ML"reset show_question_marks"(*>*)
+subsection {*Qualified names*}
+
+text{* If there are multiple declarations of the same name, Isabelle prints
+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 \verb!short_names!, typically
+in \texttt{ROOT.ML}:
+\begin{verbatim}
+set short_names;
+\end{verbatim}
+*}
+
subsection {*Variable names\label{sec:varnames}*}
text{* It sometimes happens that you want to change the name of a