# HG changeset patch
# User wenzelm
# Date 1752328898 -7200
# Node ID df2d774bcf210ec1853435a217d1dc6f9175ff34
# Parent  86915cddda0853a33e93eb5a6abba27edab1bcdb
proper thm ord that conforms to Thm.eq_thm_prop (amending f5fd9b41188a): relevant for declarations in a locale contex with assumptions, e.g. "locale test = assumes True begin declare refl [rule del] end";

diff -r 86915cddda08 -r df2d774bcf21 src/Pure/bires.ML
--- a/src/Pure/bires.ML	Sat Jul 12 13:05:04 2025 +0200
+++ b/src/Pure/bires.ML	Sat Jul 12 16:01:38 2025 +0200
@@ -161,28 +161,28 @@
   {kind = kind, tag = next_tag next tag, info = info};
 
 
-abstype 'a decls = Decls of {next: int, rules: 'a decl list Thmtab.table}
+abstype 'a decls = Decls of {next: int, rules: 'a decl list Proptab.table}
 with
 
 local
 
 fun dup_decls (Decls {rules, ...}) (thm, decl) =
-  member decl_eq_kind (Thmtab.lookup_list rules thm) decl;
+  member decl_eq_kind (Proptab.lookup_list rules thm) decl;
 
 fun add_decls (thm, decl) (Decls {next, rules}) =
   let
     val decl' = next_decl next decl;
-    val decls' = Decls {next = next - 1, rules = Thmtab.cons_list (thm, decl') rules};
+    val decls' = Decls {next = next - 1, rules = Proptab.cons_list (thm, decl') rules};
   in (decl', decls') end;
 
 in
 
-fun has_decls (Decls {rules, ...}) = Thmtab.defined rules;
+fun has_decls (Decls {rules, ...}) = Proptab.defined rules;
 
-fun get_decls (Decls {rules, ...}) = Thmtab.lookup_list rules;
+fun get_decls (Decls {rules, ...}) = Proptab.lookup_list rules;
 
 fun dest_decls (Decls {rules, ...}) pred =
-  build (rules |> Thmtab.fold (fn (th, ds) => ds |> fold (fn d => pred (th, d) ? cons (th, d))))
+  build (rules |> Proptab.fold (fn (th, ds) => ds |> fold (fn d => pred (th, d) ? cons (th, d))))
   |> sort (decl_ord o apply2 #2);
 
 fun pretty_decls ctxt kinds decls =
@@ -201,9 +201,9 @@
 fun remove_decls thm (decls as Decls {next, rules}) =
   (case get_decls decls thm of
     [] => ([], decls)
-  | old_decls => (old_decls, Decls {next = next, rules = Thmtab.delete thm rules}));
+  | old_decls => (old_decls, Decls {next = next, rules = Proptab.delete thm rules}));
 
-val empty_decls = Decls {next = ~1, rules = Thmtab.empty};
+val empty_decls = Decls {next = ~1, rules = Proptab.empty};
 
 end;
 
diff -r 86915cddda08 -r df2d774bcf21 src/Pure/cterm_items.ML
--- a/src/Pure/cterm_items.ML	Sat Jul 12 13:05:04 2025 +0200
+++ b/src/Pure/cterm_items.ML	Sat Jul 12 16:01:38 2025 +0200
@@ -43,6 +43,12 @@
 end;
 
 
+structure Proptab = Table
+(
+  type key = thm
+  val ord = pointer_eq_ord (Term_Ord.fast_term_ord o apply2 Thm.full_prop_of)
+);
+
 structure Thmtab:
 sig
   include TABLE