src/Pure/sign.ML
changeset 22796 34c316d7b630
parent 22765 2a3840aa2ffd
child 22811 eb59c9b76d52
     1.1 --- a/src/Pure/sign.ML	Thu Apr 26 12:00:01 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Apr 26 12:00:05 2007 +0200
     1.3 @@ -61,14 +61,6 @@
     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_classes: bool -> xstring list -> theory -> theory
     1.8 -  val hide_classes_i: bool -> string list -> theory -> theory
     1.9 -  val hide_types: bool -> xstring list -> theory -> theory
    1.10 -  val hide_types_i: bool -> string list -> theory -> theory
    1.11 -  val hide_consts: bool -> xstring list -> theory -> theory
    1.12 -  val hide_consts_i: bool -> string list -> theory -> theory
    1.13 -  val hide_names: bool -> string * xstring list -> theory -> theory
    1.14 -  val hide_names_i: bool -> string * string list -> theory -> theory
    1.15  end
    1.16  
    1.17  signature SIGN =
    1.18 @@ -186,6 +178,14 @@
    1.19    val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
    1.20    val add_abbrev: string -> bstring * term -> theory -> (term * term) * theory
    1.21    include SIGN_THEORY
    1.22 +  val hide_classes: bool -> xstring list -> theory -> theory
    1.23 +  val hide_classes_i: bool -> string list -> theory -> theory
    1.24 +  val hide_types: bool -> xstring list -> theory -> theory
    1.25 +  val hide_types_i: bool -> string list -> theory -> theory
    1.26 +  val hide_consts: bool -> xstring list -> theory -> theory
    1.27 +  val hide_consts_i: bool -> string list -> theory -> theory
    1.28 +  val hide_names: bool -> string * xstring list -> theory -> theory
    1.29 +  val hide_names_i: bool -> string * string list -> theory -> theory
    1.30  end
    1.31  
    1.32  structure Sign: SIGN =