# HG changeset patch
# User wenzelm
# Date 1684090448 -7200
# Node ID 2c3f4d80abfb47b62881a603bd31c2f68637f194
# Parent  6c6eae08ff87c12c0d44a87372f879587ad3d8ae
more standard merge order, following logical structure of imports rather than physical serials;

diff -r 6c6eae08ff87 -r 2c3f4d80abfb src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun May 14 13:15:52 2023 +0200
+++ b/src/Pure/Isar/generic_target.ML	Sun May 14 20:54:08 2023 +0200
@@ -167,18 +167,18 @@
 
 structure Foundation_Interpretations = Theory_Data
 (
-  type T = (binding * (term * term list) -> Context.generic -> Context.generic) Inttab.table;
-  val empty = Inttab.empty;
-  val merge = Inttab.merge (K true);
+  type T = ((binding * (term * term list) -> Context.generic -> Context.generic) * stamp) list
+  val empty = [];
+  val merge = Library.merge (eq_snd (op =));
 );
 
 fun add_foundation_interpretation f =
-  Foundation_Interpretations.map (Inttab.update_new (serial (), f));
+  Foundation_Interpretations.map (cons (f, stamp ()));
 
 fun foundation_interpretation binding_const_params lthy =
   let
     val interps = Foundation_Interpretations.get (Proof_Context.theory_of lthy);
-    val interp = Inttab.fold (fn (_, f) => f binding_const_params) interps;
+    val interp = fold (fn (f, _) => f binding_const_params) interps;
   in
     lthy
     |> Local_Theory.background_theory (Context.theory_map interp)