src/Pure/sign.ML
changeset 59923 b21c82422d65
parent 59896 e563b0ee0331
child 59939 7d46aa03696e
--- a/src/Pure/sign.ML	Fri Apr 03 21:25:55 2015 +0200
+++ b/src/Pure/sign.ML	Sat Apr 04 14:04:11 2015 +0200
@@ -111,7 +111,8 @@
   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 private_scope: Binding.scope -> theory -> theory
+  val private: Position.T -> theory -> theory
   val concealed: theory -> theory
   val hide_class: bool -> string -> theory -> theory
   val hide_type: bool -> string -> theory -> theory
@@ -522,6 +523,7 @@
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
 
+val private_scope = map_naming o Name_Space.private_scope;
 val private = map_naming o Name_Space.private;
 val concealed = map_naming Name_Space.concealed;