# HG changeset patch
# User krauss
# Date 1286745384 -7200
# Node ID c9cbc16e93ce0b2dca79b2bd881f359c482543bb
# Parent  2474347538b812daebe2294dcc0ee56132a7d078
do not mention unqualified names, now that 'global' and 'local' are gone

diff -r 2474347538b8 -r c9cbc16e93ce doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Sun Oct 10 16:34:20 2010 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Sun Oct 10 23:16:24 2010 +0200
@@ -1209,8 +1209,7 @@
 
   \item @{command "hide_class"}~@{text names} fully removes class
   declarations from a given name space; with the @{text "(open)"}
-  option, only the base name is hidden.  Global (unqualified) names
-  may never be hidden.
+  option, only the base name is hidden.
 
   Note that hiding name space accesses has no impact on logical
   declarations --- they remain valid internally.  Entities that are no
diff -r 2474347538b8 -r c9cbc16e93ce doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Sun Oct 10 16:34:20 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sun Oct 10 23:16:24 2010 +0200
@@ -1252,8 +1252,7 @@
 
   \item \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}~\isa{names} fully removes class
   declarations from a given name space; with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}
-  option, only the base name is hidden.  Global (unqualified) names
-  may never be hidden.
+  option, only the base name is hidden.
 
   Note that hiding name space accesses has no impact on logical
   declarations --- they remain valid internally.  Entities that are no