# 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;