Theory.hide_space_i true;

--- a/src/Pure/Isar/isar_thy.ML	Fri Dec 21 23:17:12 2001 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Fri Dec 21 23:17:35 2001 +0100
@@ -250,7 +250,7 @@
         val names = map (intern sg kind) xnames;
         val bads = filter_out (check sg) names;
       in
-        if null bads then Theory.hide_space_i (kind, names) thy
+        if null bads then Theory.hide_space_i true (kind, names) thy
         else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
       end
   | None => error ("Bad name space specification: " ^ quote kind));