renamed hide_classes/types/consts to hide_XXX_i;
authorwenzelm
Sat Jun 11 22:15:54 2005 +0200 (2005-06-11)
changeset 1636996d73621fabb
parent 16368 a06868ebeb0f
child 16370 033d890fe91f
renamed hide_classes/types/consts to hide_XXX_i;
added separate hide_classes/types/consts;
refer to name spaces values instead of names;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Sat Jun 11 22:15:53 2005 +0200
     1.2 +++ b/src/Pure/theory.ML	Sat Jun 11 22:15:54 2005 +0200
     1.3 @@ -94,11 +94,12 @@
     1.4    val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
     1.5      theory -> theory
     1.6    val restore_naming: theory -> theory -> theory
     1.7 -  val hide_space: bool -> string * xstring list -> theory -> theory
     1.8 -  val hide_space_i: bool -> string * string list -> theory -> theory
     1.9 -  val hide_classes: bool -> string list -> theory -> theory
    1.10 -  val hide_types: bool -> string list -> theory -> theory
    1.11 -  val hide_consts: bool -> string list -> theory -> theory
    1.12 +  val hide_classes: bool -> xstring list -> theory -> theory
    1.13 +  val hide_classes_i: bool -> string list -> theory -> theory
    1.14 +  val hide_types: bool -> xstring list -> theory -> theory
    1.15 +  val hide_types_i: bool -> string list -> theory -> theory
    1.16 +  val hide_consts: bool -> xstring list -> theory -> theory
    1.17 +  val hide_consts_i: bool -> string list -> theory -> theory
    1.18    val add_name: string -> theory -> theory
    1.19    val copy: theory -> theory
    1.20    val prep_ext: theory -> theory
    1.21 @@ -235,11 +236,12 @@
    1.22  val custom_accesses        = ext_sign Sign.custom_accesses;
    1.23  val set_policy             = ext_sign Sign.set_policy;
    1.24  val restore_naming         = ext_sign Sign.restore_naming o sign_of;
    1.25 -val hide_space             = ext_sign o Sign.hide_space;
    1.26 -val hide_space_i           = ext_sign o Sign.hide_space_i;
    1.27 -fun hide_classes b         = curry (hide_space_i b) Sign.classK;
    1.28 -fun hide_types b           = curry (hide_space_i b) Sign.typeK;
    1.29 -fun hide_consts b          = curry (hide_space_i b) Sign.constK;
    1.30 +val hide_classes           = ext_sign o Sign.hide_classes;
    1.31 +val hide_classes_i         = ext_sign o Sign.hide_classes_i;
    1.32 +val hide_types             = ext_sign o Sign.hide_types;
    1.33 +val hide_types_i           = ext_sign o Sign.hide_types_i;
    1.34 +val hide_consts            = ext_sign o Sign.hide_consts;
    1.35 +val hide_consts_i          = ext_sign o Sign.hide_consts_i;
    1.36  val add_name               = ext_sign Sign.add_name;
    1.37  val copy                   = ext_sign (K Sign.copy) ();
    1.38  val prep_ext               = ext_sign (K Sign.prep_ext) ();