# HG changeset patch
# User wenzelm
# Date 1574516924 -3600
# Node ID 25b872d1d4219703607f01c4a9032c4d9633dfee
# Parent  7db80bd16f1cdad70f27165674d83f809389e263
clarified signature;

diff -r 7db80bd16f1c -r 25b872d1d421 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sat Nov 23 11:45:02 2019 +0100
+++ b/src/Pure/pure_thy.ML	Sat Nov 23 14:48:44 2019 +0100
@@ -78,7 +78,7 @@
   ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"];
 
 val _ = Theory.setup
-  (Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
+  (Sign.theory_naming #>
    Old_Appl_Syntax.put false #>
    Sign.add_types_global
    [(Binding.make ("fun", \<^here>), 2, NoSyn),
diff -r 7db80bd16f1c -r 25b872d1d421 src/Pure/sign.ML
--- 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;
diff -r 7db80bd16f1c -r 25b872d1d421 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat Nov 23 11:45:02 2019 +0100
+++ b/src/Pure/theory.ML	Sat Nov 23 14:48:44 2019 +0100
@@ -194,7 +194,7 @@
       thy
       |> init_markup (name, pos)
       |> Sign.local_path
-      |> Sign.map_naming (Name_Space.set_theory_name (Long_Name.base_name name))
+      |> Sign.theory_naming
       |> apply_wrappers wrappers
       |> tap (Syntax.force_syntax o Sign.syn_of)
     end;