tuned signature;
authorwenzelm
Wed Apr 01 18:17:44 2015 +0200 (2015-04-01)
changeset 59896e563b0ee0331
parent 59895 a68a0fec288d
child 59897 d1e7f56bcd79
tuned signature;
src/Pure/Isar/proof_context.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 01 18:16:53 2015 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 01 18:17:44 2015 +0200
     1.3 @@ -36,6 +36,7 @@
     1.4    val full_name: Proof.context -> binding -> string
     1.5    val get_scope: Proof.context -> Binding.scope option
     1.6    val new_scope: Proof.context -> Binding.scope * Proof.context
     1.7 +  val private: Binding.scope -> Proof.context -> Proof.context
     1.8    val concealed: Proof.context -> Proof.context
     1.9    val class_space: Proof.context -> Name_Space.T
    1.10    val type_space: Proof.context -> Name_Space.T
    1.11 @@ -315,6 +316,7 @@
    1.12      val ctxt' = map_naming (K naming') ctxt;
    1.13    in (scope, ctxt') end;
    1.14  
    1.15 +val private = map_naming o Name_Space.private;
    1.16  val concealed = map_naming Name_Space.concealed;
    1.17  
    1.18  
     2.1 --- a/src/Pure/sign.ML	Wed Apr 01 18:16:53 2015 +0200
     2.2 +++ b/src/Pure/sign.ML	Wed Apr 01 18:17:44 2015 +0200
     2.3 @@ -111,6 +111,7 @@
     2.4    val mandatory_path: string -> theory -> theory
     2.5    val qualified_path: bool -> binding -> theory -> theory
     2.6    val local_path: theory -> theory
     2.7 +  val private: Binding.scope -> theory -> theory
     2.8    val concealed: theory -> theory
     2.9    val hide_class: bool -> string -> theory -> theory
    2.10    val hide_type: bool -> string -> theory -> theory
    2.11 @@ -521,6 +522,7 @@
    2.12  
    2.13  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
    2.14  
    2.15 +val private = map_naming o Name_Space.private;
    2.16  val concealed = map_naming Name_Space.concealed;
    2.17  
    2.18