--- a/src/Pure/sign.ML Sat Nov 23 11:45:02 2019 +0100
+++ b/src/Pure/sign.ML Sat Nov 23 14:48:44 2019 +0100
@@ -110,6 +110,7 @@
val mandatory_path: string -> theory -> theory
val qualified_path: bool -> binding -> theory -> theory
val local_path: theory -> theory
+ val theory_naming: theory -> theory
val private_scope: Binding.scope -> theory -> theory
val private: Position.T -> theory -> theory
val qualified_scope: Binding.scope -> theory -> theory
@@ -524,6 +525,8 @@
fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
+fun theory_naming thy = thy |> map_naming (Name_Space.set_theory_name (Context.theory_name thy));
+
val private_scope = map_naming o Name_Space.private_scope;
val private = map_naming o Name_Space.private;
val qualified_scope = map_naming o Name_Space.qualified_scope;