# HG changeset patch
# User wenzelm
# Date 1753041007 -7200
# Node ID a299162422f0e28b9f1dca72708a249dc567d3d4
# Parent  051177553f16aca669e2951609a8f71e11db9781
clarified decl_ord wrt. kind_ord;

diff -r 051177553f16 -r a299162422f0 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Jul 20 20:31:04 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Jul 20 21:50:07 2025 +0200
@@ -307,10 +307,10 @@
       let
         fun add stature th = Termtab.update (normalize_vars (Thm.prop_of th), stature)
 
-        fun claset_rules kind =
-          map #1 (Classical.dest_decls ctxt (fn (_, {kind = kind', ...}) => kind = kind'));
-
-        val intros = claset_rules Bires.intro_bang_kind @ claset_rules Bires.intro_kind;
+        val intros =
+          Classical.dest_decls ctxt (fn (_, {kind, ...}) =>
+            kind = Bires.intro_bang_kind orelse kind = Bires.intro_kind)
+          |> map #1
 (* Add once it is used:
         val elims =
           (claset_rules Bires.elim_bang_kind @ claset_rules Bires.elim_kind)
diff -r 051177553f16 -r a299162422f0 src/Pure/bires.ML
--- a/src/Pure/bires.ML	Sun Jul 20 20:31:04 2025 +0200
+++ b/src/Pure/bires.ML	Sun Jul 20 21:50:07 2025 +0200
@@ -149,6 +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;
+
 fun kind_name (Kind {is_elim, make_elim, ...}) =
   if is_elim andalso make_elim then "destruction rule"
   else if is_elim then "elimination rule"
@@ -177,7 +179,10 @@
 
 type 'a decl = {kind: kind, tag: tag, info: 'a};
 
-fun decl_ord (args: 'a decl * 'a decl) = tag_index_ord (apply2 #tag args);
+fun decl_ord (args: 'a decl * 'a decl) =
+  (case kind_ord (apply2 #kind args) of
+    EQUAL => tag_index_ord (apply2 #tag args)
+  | ord => ord);
 
 fun decl_eq_kind ({kind, ...}: 'a decl, {kind = kind', ...}: 'a decl) = kind = kind';