# HG changeset patch
# User wenzelm
# Date 1683282863 -7200
# Node ID f68df517e8c4350b67e7c31fb70dbef6cfb29c7b
# Parent  8ce2425a7c94dc9adaa9be04c1c83ff3c3e545d3
tuned;

diff -r 8ce2425a7c94 -r f68df517e8c4 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri May 05 12:17:29 2023 +0200
+++ b/src/Pure/General/name_space.ML	Fri May 05 12:34:23 2023 +0200
@@ -115,6 +115,9 @@
   pos: Position.T,
   serial: serial};
 
+fun eq_entry_serial (entry1: entry, entry2: entry) : bool =
+  #serial entry1 = #serial entry2;
+
 fun entry_markup def kind (name, {pos, serial, ...}: entry) =
   Position.make_entity_markup def serial kind (name, pos);
 
@@ -389,7 +392,7 @@
         then raise Long_Name.Chunks.SAME
         else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
     val entries' = (entries1, entries2) |> Change_Table.join (fn name => fn (entry1, entry2) =>
-      if #serial entry1 = #serial entry2 then raise Change_Table.SAME
+      if eq_entry_serial (entry1, entry2) then raise Change_Table.SAME
       else err_dup kind' (name, entry1) (name, entry2) Position.none);
     val aliases' = Symtab.merge_list (op =) (aliases1, aliases2);
   in make_name_space (kind', internals', entries', aliases') end;