src/Pure/theory.ML
changeset 16369 96d73621fabb
parent 16339 b02b6da609c3
child 16443 82a116532e3e
     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) ();