# HG changeset patch
# User wenzelm
# Date 1008973055 -3600
# Node ID afc6ffffeb11ebb32777e4f49fc9ed51d1dcec8b
# Parent  0361fd72f1a7a7d02c6d3d5ecefbabe889bd62b5
Theory.hide_space_i true;

diff -r 0361fd72f1a7 -r afc6ffffeb11 src/Pure/Isar/isar_thy.ML
--- 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));