# HG changeset patch
# User wenzelm
# Date 1752238549 -7200
# Node ID d4da7d857bb7eaa56e1bb80d602818016bf10f70
# Parent  ebfb0e011c950e11cd6a22e39a0e81d86dde801b
clarified signature;

diff -r ebfb0e011c95 -r d4da7d857bb7 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- 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:
diff -r ebfb0e011c95 -r d4da7d857bb7 src/Provers/classical.ML
--- 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;