--- 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);
--- 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),
--- 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;
--- 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;