--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 11 14:37:23 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 11 14:55:49 2025 +0200
@@ -307,9 +307,8 @@
let
fun add stature th = Termtab.update (normalize_vars (Thm.prop_of th), stature)
- val claset_decls = Classical.get_decls ctxt;
fun claset_rules kind =
- map #1 (Bires.dest_decls claset_decls (fn (_, {kind = kind', ...}) => kind = 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;
(* Add once it is used:
--- a/src/Provers/classical.ML Fri Jul 11 14:37:23 2025 +0200
+++ b/src/Provers/classical.ML Fri Jul 11 14:55:49 2025 +0200
@@ -108,7 +108,7 @@
unsafe_netpair: Bires.netpair,
dup_netpair: Bires.netpair,
extra_netpair: Bires.netpair}
- val get_decls: Proof.context -> decls
+ val dest_decls: Proof.context -> ((thm * decl) -> bool) -> (thm * decl) list
val get_cs: Context.generic -> claset
val map_cs: (claset -> claset) -> Context.generic -> Context.generic
val safe_dest: int option -> attribute
@@ -488,7 +488,7 @@
val claset_of = Claset.get o Context.Proof;
val rep_claset_of = rep_cs o claset_of;
-val get_decls = #decls o rep_claset_of;
+val dest_decls = Bires.dest_decls o #decls o rep_claset_of;
val get_cs = Claset.get;
val map_cs = Claset.map;