renamed hide_classes/types/consts to hide_XXX_i;
added separate hide_classes/types/consts;
refer to name spaces values instead of names;
--- a/src/Pure/theory.ML Sat Jun 11 22:15:53 2005 +0200
+++ b/src/Pure/theory.ML Sat Jun 11 22:15:54 2005 +0200
@@ -94,11 +94,12 @@
val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
theory -> theory
val restore_naming: theory -> theory -> theory
- val hide_space: bool -> string * xstring list -> theory -> theory
- val hide_space_i: bool -> string * string list -> theory -> theory
- val hide_classes: bool -> string list -> theory -> theory
- val hide_types: bool -> string list -> theory -> theory
- val hide_consts: bool -> string list -> theory -> theory
+ val hide_classes: bool -> xstring list -> theory -> theory
+ val hide_classes_i: bool -> string list -> theory -> theory
+ val hide_types: bool -> xstring list -> theory -> theory
+ val hide_types_i: bool -> string list -> theory -> theory
+ val hide_consts: bool -> xstring list -> theory -> theory
+ val hide_consts_i: bool -> string list -> theory -> theory
val add_name: string -> theory -> theory
val copy: theory -> theory
val prep_ext: theory -> theory
@@ -235,11 +236,12 @@
val custom_accesses = ext_sign Sign.custom_accesses;
val set_policy = ext_sign Sign.set_policy;
val restore_naming = ext_sign Sign.restore_naming o sign_of;
-val hide_space = ext_sign o Sign.hide_space;
-val hide_space_i = ext_sign o Sign.hide_space_i;
-fun hide_classes b = curry (hide_space_i b) Sign.classK;
-fun hide_types b = curry (hide_space_i b) Sign.typeK;
-fun hide_consts b = curry (hide_space_i b) Sign.constK;
+val hide_classes = ext_sign o Sign.hide_classes;
+val hide_classes_i = ext_sign o Sign.hide_classes_i;
+val hide_types = ext_sign o Sign.hide_types;
+val hide_types_i = ext_sign o Sign.hide_types_i;
+val hide_consts = ext_sign o Sign.hide_consts;
+val hide_consts_i = ext_sign o Sign.hide_consts_i;
val add_name = ext_sign Sign.add_name;
val copy = ext_sign (K Sign.copy) ();
val prep_ext = ext_sign (K Sign.prep_ext) ();