diff -r 91dfe7dccfdf -r 3165bc303f66 doc-src/Classes/Thy/document/Classes.tex
--- a/doc-src/Classes/Thy/document/Classes.tex	Mon May 31 19:36:13 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex	Mon May 31 21:06:57 2010 +0200
@@ -792,8 +792,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Isabelle locales support a concept of local definitions
-  in locales:%
+Isabelle locales are targets which support local definitions:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %