# HG changeset patch
# User wenzelm
# Date 1753103400 -7200
# Node ID 372273ab6ebbc8b72f74cf141442af6d3afc2bf0
# Parent  72707b8447344d5903f264f5c6ac12cef232c473
clarified natural decl_ord vs. slightly odd merge_decl_ord, following the historic status-quo of 53e56e6a67c3, which originally stems from c06d01f75764;

diff -r 72707b844734 -r 372273ab6ebb src/Pure/bires.ML
--- a/src/Pure/bires.ML	Mon Jul 21 12:57:58 2025 +0200
+++ b/src/Pure/bires.ML	Mon Jul 21 15:10:00 2025 +0200
@@ -45,7 +45,7 @@
   val kind_title: kind -> string
 
   type 'a decl = {kind: kind, tag: tag, info: 'a}
-  val decl_ord: {reverse_index: bool} -> 'a decl ord
+  val decl_ord: 'a decl ord
   val decl_eq_kind: 'a decl * 'a decl -> bool
   type 'a decls
   val has_decls: 'a decls -> thm -> bool
@@ -149,7 +149,8 @@
 fun kind_is_elim (Kind {is_elim, ...}) = is_elim;
 fun kind_make_elim (Kind {make_elim, ...}) = make_elim ? Tactic.make_elim;
 
-val kind_ord = int_ord o apply2 kind_index ||| bool_ord o apply2 kind_is_elim;
+val kind_index_ord = int_ord o apply2 kind_index;
+val kind_elim_ord = bool_ord o apply2 kind_is_elim;
 
 fun kind_name (Kind {is_elim, make_elim, ...}) =
   if is_elim andalso make_elim then "destruction rule"
@@ -179,9 +180,14 @@
 
 type 'a decl = {kind: kind, tag: tag, info: 'a};
 
-fun decl_ord {reverse_index} (args: 'a decl * 'a decl) =
-  (case kind_ord (apply2 #kind args) of
-    EQUAL => (reverse_index ? rev_order) (tag_index_ord (apply2 #tag args))
+fun decl_ord (args: 'a decl * 'a decl) =
+  (case kind_index_ord (apply2 #kind args) of
+    EQUAL => tag_index_ord (apply2 #tag args)
+  | ord => ord);
+
+fun decl_merge_ord (args: 'a decl * 'a decl) =
+  (case kind_elim_ord (apply2 #kind args) of
+    EQUAL => rev_order (tag_index_ord (apply2 #tag args))
   | ord => ord);
 
 fun decl_eq_kind ({kind, ...}: 'a decl, {kind = kind', ...}: 'a decl) = kind = kind';
@@ -214,8 +220,7 @@
   build (rules |> Proptab.fold (fn (th, ds) => ds |> fold (fn d => pred (th, d) ? cons (th, d))))
   |> 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 dest_decls decls = dest_decls_ord decl_ord decls;
 
 fun pretty_decls ctxt decls =
   kind_domain |> map_filter (fn kind =>
@@ -226,7 +231,7 @@
           (map (Thm.pretty_thm_item ctxt o #1) ds))));
 
 fun merge_decls (decls1, decls2) =
-  decls1 |> fold_map add_decls (dest_decls' decls2 (not o dup_decls decls1));
+  decls1 |> fold_map add_decls (dest_decls_ord decl_merge_ord decls2 (not o dup_decls decls1));
 
 fun extend_decls (thm, decl) decls =
   if dup_decls decls (thm, decl) then (NONE, decls)