# HG changeset patch
# User wenzelm
# Date 1594990615 -7200
# Node ID 4ed33ea8d9579cf378c2e6363abb2acdf21a25cc
# Parent  912f13865596193883107186b4427028bb781916
prefer conservative extend/merge of theory naming;

diff -r 912f13865596 -r 4ed33ea8d957 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu Jul 16 22:24:03 2020 +0200
+++ b/src/Pure/General/name_space.ML	Fri Jul 17 14:56:55 2020 +0200
@@ -488,9 +488,9 @@
 struct
   type T = naming;
   val empty = global_naming;
-  fun extend _ = global_naming;
-  fun merge _ = global_naming;
   fun init _ = local_naming;
+  val extend = I;
+  val merge = #1;
 end;
 
 structure Global_Naming = Theory_Data(Data_Args);
diff -r 912f13865596 -r 4ed33ea8d957 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Jul 16 22:24:03 2020 +0200
+++ b/src/Pure/pure_thy.ML	Fri Jul 17 14:56:55 2020 +0200
@@ -78,7 +78,7 @@
   ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"];
 
 val _ = Theory.setup
-  (Sign.theory_naming #>
+  (Sign.init_naming #>
    Old_Appl_Syntax.put false #>
    Sign.add_types_global
    [(Binding.make ("fun", \<^here>), 2, NoSyn),
diff -r 912f13865596 -r 4ed33ea8d957 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Jul 16 22:24:03 2020 +0200
+++ b/src/Pure/sign.ML	Fri Jul 17 14:56:55 2020 +0200
@@ -110,7 +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 init_naming: theory -> theory
   val private_scope: Binding.scope -> theory -> theory
   val private: Position.T -> theory -> theory
   val qualified_scope: Binding.scope -> theory -> theory
@@ -525,8 +525,11 @@
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
 
-fun theory_naming thy = thy
-  |> map_naming (Name_Space.set_theory_long_name (Context.theory_long_name thy));
+fun init_naming thy =
+  let
+    val theory_naming = Name_Space.global_naming
+      |> Name_Space.set_theory_long_name (Context.theory_long_name thy);
+  in map_naming (K theory_naming) thy end;
 
 val private_scope = map_naming o Name_Space.private_scope;
 val private = map_naming o Name_Space.private;
diff -r 912f13865596 -r 4ed33ea8d957 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Jul 16 22:24:03 2020 +0200
+++ b/src/Pure/theory.ML	Fri Jul 17 14:56:55 2020 +0200
@@ -170,7 +170,7 @@
 
 fun join_theory [] = raise List.Empty
   | join_theory [thy] = thy
-  | join_theory thys = foldl1 Context.join_thys thys |> Sign.restore_naming (hd thys);
+  | join_theory thys = foldl1 Context.join_thys thys;
 
 
 (* begin/end theory *)
@@ -193,8 +193,8 @@
     in
       thy
       |> init_markup (name, pos)
+      |> Sign.init_naming
       |> Sign.local_path
-      |> Sign.theory_naming
       |> apply_wrappers wrappers
       |> tap (Syntax.force_syntax o Sign.syn_of)
     end;