# HG changeset patch
# User wenzelm
# Date 1427905064 -7200
# Node ID e563b0ee0331d9645e9a77119b35fa164638221b
# Parent  a68a0fec288d3691448d4af14a12ec11856ebd63
tuned signature;

diff -r a68a0fec288d -r e563b0ee0331 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Apr 01 18:16:53 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Apr 01 18:17:44 2015 +0200
@@ -36,6 +36,7 @@
   val full_name: Proof.context -> binding -> string
   val get_scope: Proof.context -> Binding.scope option
   val new_scope: Proof.context -> Binding.scope * Proof.context
+  val private: Binding.scope -> Proof.context -> Proof.context
   val concealed: Proof.context -> Proof.context
   val class_space: Proof.context -> Name_Space.T
   val type_space: Proof.context -> Name_Space.T
@@ -315,6 +316,7 @@
     val ctxt' = map_naming (K naming') ctxt;
   in (scope, ctxt') end;
 
+val private = map_naming o Name_Space.private;
 val concealed = map_naming Name_Space.concealed;
 
 
diff -r a68a0fec288d -r e563b0ee0331 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Apr 01 18:16:53 2015 +0200
+++ b/src/Pure/sign.ML	Wed Apr 01 18:17:44 2015 +0200
@@ -111,6 +111,7 @@
   val mandatory_path: string -> theory -> theory
   val qualified_path: bool -> binding -> theory -> theory
   val local_path: theory -> theory
+  val private: Binding.scope -> theory -> theory
   val concealed: theory -> theory
   val hide_class: bool -> string -> theory -> theory
   val hide_type: bool -> string -> theory -> theory
@@ -521,6 +522,7 @@
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
 
+val private = map_naming o Name_Space.private;
 val concealed = map_naming Name_Space.concealed;