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