# HG changeset patch
# User wenzelm
# Date 1681202704 -7200
# Node ID a1bf8f706bc11201d7afa24e5b6474c1053628c5
# Parent  aa814dc5a685a4619c958c5b1edd17760876801b
tuned;

diff -r aa814dc5a685 -r a1bf8f706bc1 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Apr 11 10:44:32 2023 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Apr 11 10:45:04 2023 +0200
@@ -346,23 +346,19 @@
 structure Idtab = Table(type key = string * term list val ord = total_ident_ord);
 
 type reg = {morphisms: morphism * morphism, pos: Position.T, serial: serial};
-type regs = reg Idtab.table;
-
-val join_regs : regs * regs -> regs =
-  Idtab.join (fn id => fn (reg1, reg2) =>
-    if #serial reg1 = #serial reg2 then raise Idtab.SAME else raise Idtab.DUP id);
+val eq_reg: reg * reg -> bool = op = o apply2 #serial;
 
 (* FIXME consolidate with locale dependencies, consider one data slot only *)
 structure Global_Registrations = Theory_Data'
 (
   (*registrations, indexed by locale name and instance;
     unique registration serial points to mixin list*)
-  type T = regs * mixins;
+  type T = reg Idtab.table * mixins;
   val empty: T = (Idtab.empty, Inttab.empty);
   fun merge old_thys =
     let
       fun recursive_merge ((regs1, mixins1), (regs2, mixins2)) : T =
-        (join_regs (regs1, regs2), merge_mixins (mixins1, mixins2))
+        (Idtab.merge eq_reg (regs1, regs2), merge_mixins (mixins1, mixins2))
         handle Idtab.DUP id =>
           (*distinct interpretations with same base: merge their mixins*)
           let