src/Pure/sign.ML
changeset 33157 56f836b9414f
parent 33097 9d501e11084a
child 33165 50c4debfd5ae
     1.1 --- a/src/Pure/sign.ML	Sun Oct 25 11:58:11 2009 +0100
     1.2 +++ b/src/Pure/sign.ML	Sun Oct 25 12:27:21 2009 +0100
     1.3 @@ -125,6 +125,7 @@
     1.4    val parent_path: theory -> theory
     1.5    val mandatory_path: string -> theory -> theory
     1.6    val local_path: theory -> theory
     1.7 +  val conceal: theory -> theory
     1.8    val restore_naming: theory -> theory -> theory
     1.9    val hide_class: bool -> string -> theory -> theory
    1.10    val hide_type: bool -> string -> theory -> theory
    1.11 @@ -618,6 +619,8 @@
    1.12  
    1.13  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
    1.14  
    1.15 +val conceal = map_naming Name_Space.conceal;
    1.16 +
    1.17  val restore_naming = map_naming o K o naming_of;
    1.18  
    1.19