# HG changeset patch
# User wenzelm
# Date 1753095478 -7200
# Node ID 72707b8447344d5903f264f5c6ac12cef232c473
# Parent  a299162422f0e28b9f1dca72708a249dc567d3d4
clarified merge order: accurately reproduce the stable status-quo from 53e56e6a67c3 --- e.g. relevant for smt proof reconstruction in (line 6705 of "$AFP/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy") of AFP/f1299d4f896c;

diff -r a299162422f0 -r 72707b844734 NEWS
--- a/NEWS	Sun Jul 20 21:50:07 2025 +0200
+++ b/NEWS	Mon Jul 21 12:57:58 2025 +0200
@@ -22,7 +22,7 @@
 intermediate [rule del] declarations. Furthermore, [dest] is now a
 proper declaration on its own account, instead of the former expansion
 [elim_format, elim]. Consequently, [rule del] no longer deletes the
-[elim_format] of the given rule, only the original rule. Rare
+[elim_format] of the given rule, only the original rule. Very rare
 INCOMPATIBILITY: tools like "blast" and "auto" may fail in unusual
 situations.
 
diff -r a299162422f0 -r 72707b844734 src/Pure/bires.ML
--- a/src/Pure/bires.ML	Sun Jul 20 21:50:07 2025 +0200
+++ b/src/Pure/bires.ML	Mon Jul 21 12:57:58 2025 +0200
@@ -45,7 +45,7 @@
   val kind_title: kind -> string
 
   type 'a decl = {kind: kind, tag: tag, info: 'a}
-  val decl_ord: 'a decl ord
+  val decl_ord: {reverse_index: bool} -> 'a decl ord
   val decl_eq_kind: 'a decl * 'a decl -> bool
   type 'a decls
   val has_decls: 'a decls -> thm -> bool
@@ -179,9 +179,9 @@
 
 type 'a decl = {kind: kind, tag: tag, info: 'a};
 
-fun decl_ord (args: 'a decl * 'a decl) =
+fun decl_ord {reverse_index} (args: 'a decl * 'a decl) =
   (case kind_ord (apply2 #kind args) of
-    EQUAL => tag_index_ord (apply2 #tag args)
+    EQUAL => (reverse_index ? rev_order) (tag_index_ord (apply2 #tag args))
   | ord => ord);
 
 fun decl_eq_kind ({kind, ...}: 'a decl, {kind = kind', ...}: 'a decl) = kind = kind';
@@ -210,9 +210,12 @@
 
 fun get_decls (Decls {rules, ...}) = Proptab.lookup_list rules;
 
-fun dest_decls (Decls {rules, ...}) pred =
+fun dest_decls_ord ord (Decls {rules, ...}) pred =
   build (rules |> Proptab.fold (fn (th, ds) => ds |> fold (fn d => pred (th, d) ? cons (th, d))))
-  |> sort (decl_ord o apply2 #2);
+  |> sort (ord o apply2 #2);
+
+fun dest_decls decls = dest_decls_ord (decl_ord {reverse_index = false}) decls;
+fun dest_decls' decls = dest_decls_ord (decl_ord {reverse_index = true}) decls;
 
 fun pretty_decls ctxt decls =
   kind_domain |> map_filter (fn kind =>
@@ -223,7 +226,7 @@
           (map (Thm.pretty_thm_item ctxt o #1) ds))));
 
 fun merge_decls (decls1, decls2) =
-  decls1 |> fold_map add_decls (rev (dest_decls decls2 (not o dup_decls decls1)));
+  decls1 |> fold_map add_decls (dest_decls' decls2 (not o dup_decls decls1));
 
 fun extend_decls (thm, decl) decls =
   if dup_decls decls (thm, decl) then (NONE, decls)