src/Pure/sign.ML

     (string * string * (string -> string * real)) list -> sg -> sg
   val add_trrules: (xstring * string) Syntax.trrule list -> sg -> sg
   val add_trrules_i: ast Syntax.trrule list -> sg -> sg
   val add_path: string -> sg -> sg
   val add_space: string * string list -> sg -> sg
-  val hide_space: string * string list -> sg -> sg
-  val hide_space_i: string * string list -> sg -> sg
+  val hide_space: bool -> string * string list -> sg -> sg
+  val hide_space_i: bool -> string * string list -> sg -> sg
   val add_name: string -> sg -> sg
   val data_kinds: data -> string list
   val merge_refs: sg_ref * sg_ref -> sg_ref
   val merge: sg * sg -> sg
   val copy: sg -> sg

 fun cond_extrn_table spaces kind tab = NameSpace.cond_extern_table (space_of spaces kind) tab;
 
 (*add / hide names*)
 fun change_space f spaces kind x = overwrite (spaces, (kind, f (space_of spaces kind, x)));
 fun add_names x = change_space NameSpace.extend x;
-fun hide_names x = change_space NameSpace.hide x;
+fun hide_names b x = change_space (NameSpace.hide b) x;
 
 (*make full names*)
 fun full _ "" = error "Attempt to declare empty name \"\""
   | full None name = name
   | full (Some path) name =

 (* change name space *)
 
 fun ext_add_space (syn, tsig, ctab, (path, spaces), data) (kind, names) =
   (syn, tsig, ctab, (path, add_names spaces kind names), data);
 
-fun ext_hide_space (syn, tsig, ctab, (path, spaces), data) (kind, xnames) =
-  (syn, tsig, ctab, (path, hide_names spaces kind (map (intrn spaces kind) xnames)), data);
-
-fun ext_hide_space_i (syn, tsig, ctab, (path, spaces), data) (kind, names) =
-  (syn, tsig, ctab, (path, hide_names spaces kind names), data);
+fun ext_hide_space (syn, tsig, ctab, (path, spaces), data) (b, (kind, xnames)) =
+  (syn, tsig, ctab, (path, hide_names b spaces kind (map (intrn spaces kind) xnames)), data);
+
+fun ext_hide_space_i (syn, tsig, ctab, (path, spaces), data) (b, (kind, names)) =
+  (syn, tsig, ctab, (path, hide_names b spaces kind names), data);
 
 
 (* signature data *)
 
 fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, cp, ext, mrg, prt)) =

 val add_tokentrfuns   = extend_sign true (ext_syn Syntax.extend_tokentrfuns) "#";
 val add_trrules       = extend_sign true ext_trrules "#";
 val add_trrules_i     = extend_sign true (ext_syn Syntax.extend_trrules_i) "#";
 val add_path          = extend_sign true ext_path "#";
 val add_space         = extend_sign true ext_add_space "#";
-val hide_space        = extend_sign true ext_hide_space "#";
-val hide_space_i      = extend_sign true ext_hide_space_i "#";
+val hide_space        = curry (extend_sign true ext_hide_space "#");
+val hide_space_i      = curry (extend_sign true ext_hide_space_i "#");
 fun init_data arg sg  = extend_sign true (ext_init_data sg) "#" arg sg;
 fun put_data k f x sg = extend_sign true (ext_put_data sg) "#" (k, f, x) sg;
 fun add_name name sg  = extend_sign true K name () sg;
 fun prep_ext sg       = extend_sign false K "#" () sg;