# HG changeset patch
# User wenzelm
# Date 1753268750 -7200
# Node ID 83b9639f5c423b2da7e6ff87c20ba918478e50fc
# Parent  a8e47bd319651982810452b2569533c1f132104c
tuned;

diff -r a8e47bd31965 -r 83b9639f5c42 src/Pure/bires.ML
--- a/src/Pure/bires.ML	Tue Jul 22 12:02:53 2025 +0200
+++ b/src/Pure/bires.ML	Wed Jul 23 13:05:50 2025 +0200
@@ -46,7 +46,6 @@
 
   type 'a decl = {kind: kind, tag: tag, info: 'a}
   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
   val get_decls: 'a decls -> thm -> 'a decl list
@@ -190,8 +189,6 @@
     EQUAL => rev_order (tag_index_ord (apply2 #tag args))
   | ord => ord);
 
-fun decl_eq_kind ({kind, ...}: 'a decl, {kind = kind', ...}: 'a decl) = kind = kind';
-
 fun next_decl next ({kind, tag, info}: 'a decl) : 'a decl =
   {kind = kind, tag = next_tag next tag, info = info};
 
@@ -201,8 +198,8 @@
 
 local
 
-fun dup_decls (Decls {rules, ...}) (thm, decl) =
-  member decl_eq_kind (Proptab.lookup_list rules thm) decl;
+fun dup_decls (Decls {rules, ...}) (thm, {kind, ...}: 'a decl) =
+  exists (fn {kind = kind', ...} => kind = kind') (Proptab.lookup_list rules thm);
 
 fun add_decls (thm, decl) (Decls {next, rules}) =
   let