src/Pure/sign.ML
changeset 33165 50c4debfd5ae
parent 33157 56f836b9414f
child 33172 61ee96bc9895
     1.1 --- a/src/Pure/sign.ML	Sun Oct 25 19:14:46 2009 +0100
     1.2 +++ b/src/Pure/sign.ML	Sun Oct 25 19:17:42 2009 +0100
     1.3 @@ -12,6 +12,7 @@
     1.4      syn: Syntax.syntax,
     1.5      tsig: Type.tsig,
     1.6      consts: Consts.T}
     1.7 +  val map_naming: (Name_Space.naming -> Name_Space.naming) -> theory -> theory
     1.8    val naming_of: theory -> Name_Space.naming
     1.9    val full_name: theory -> binding -> string
    1.10    val full_name_path: theory -> string -> binding -> string
    1.11 @@ -125,7 +126,6 @@
    1.12    val parent_path: theory -> theory
    1.13    val mandatory_path: string -> theory -> theory
    1.14    val local_path: theory -> theory
    1.15 -  val conceal: theory -> theory
    1.16    val restore_naming: theory -> theory -> theory
    1.17    val hide_class: bool -> string -> theory -> theory
    1.18    val hide_type: bool -> string -> theory -> theory
    1.19 @@ -619,8 +619,6 @@
    1.20  
    1.21  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
    1.22  
    1.23 -val conceal = map_naming Name_Space.conceal;
    1.24 -
    1.25  val restore_naming = map_naming o K o naming_of;
    1.26  
    1.27