# HG changeset patch
# User wenzelm
# Date 1723642229 -7200
# Node ID 29734511c661a4f418a16b7be1632870be8b664c
# Parent  552cdee5cd431493db57a5034f053a4022471b23
clarified signature;

diff -r 552cdee5cd43 -r 29734511c661 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Aug 14 13:51:36 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Aug 14 15:30:29 2024 +0200
@@ -300,7 +300,7 @@
 
 (* TODO: rewrite to use nets and/or to reuse existing data structures *)
 fun clasimpset_rule_table_of ctxt =
-  let val simps = ctxt |> simpset_of |> dest_ss |> #simps in
+  let val simps = ctxt |> simpset_of |> Simplifier.dest_simps in
     if length simps >= max_simps_for_clasimpset then
       Termtab.empty
     else
diff -r 552cdee5cd43 -r 29734511c661 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Wed Aug 14 13:51:36 2024 +0200
+++ b/src/Pure/Isar/element.ML	Wed Aug 14 15:30:29 2024 +0200
@@ -430,7 +430,8 @@
   | eq_morphism ctxt0 thms =
       let
         val simpset = Raw_Simplifier.simpset_of (Raw_Simplifier.init_simpset thms ctxt0);
-        val simps = map (decomp_simp ctxt0 o Thm.full_prop_of) (Raw_Simplifier.dest_simps simpset);
+        val simps =
+          map (decomp_simp ctxt0 o Thm.full_prop_of o #2) (Raw_Simplifier.dest_simps simpset);
 
         fun rewrite_term thy = Pattern.rewrite_term thy simps [];
         val rewrite =
diff -r 552cdee5cd43 -r 29734511c661 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Wed Aug 14 13:51:36 2024 +0200
+++ b/src/Pure/raw_simplifier.ML	Wed Aug 14 15:30:29 2024 +0200
@@ -25,15 +25,6 @@
   type simpset
   val empty_ss: simpset
   val merge_ss: simpset * simpset -> simpset
-  val dest_ss: simpset ->
-   {simps: (Thm_Name.T * thm) list,
-    simprocs: (string * term list) list,
-    congs: (cong_name * thm) list,
-    weak_congs: cong_name list,
-    loopers: string list,
-    unsafe_solvers: string list,
-    safe_solvers: string list}
-  val dest_simps: simpset -> thm list
   type simproc
   val cert_simproc: theory ->
     {name: string, lhss: term list, proc: proc Morphism.entity, identifier: thm list} -> simproc
@@ -72,6 +63,16 @@
 sig
   include BASIC_RAW_SIMPLIFIER
   exception SIMPLIFIER of string * thm list
+  val dest_simps: simpset -> (Thm_Name.T * thm) list
+  val dest_congs: simpset -> (cong_name * thm) list
+  val dest_ss: simpset ->
+   {simps: (Thm_Name.T * thm) list,
+    simprocs: (string * term list) list,
+    congs: (cong_name * thm) list,
+    weak_congs: cong_name list,
+    loopers: string list,
+    unsafe_solvers: string list,
+    safe_solvers: string list}
   val add_proc: simproc -> Proof.context -> Proof.context
   val del_proc: simproc -> Proof.context -> Proof.context
   type trace_ops
@@ -288,23 +289,26 @@
 
 fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
 
+fun dest_simps (Simpset ({rules, ...}, _)) =
+  Net.entries rules
+  |> map (fn {name, thm, ...} => (name, thm));
+
+fun dest_congs (Simpset (_, {congs, ...})) = Congtab.dest (#1 congs);
+
 fun dest_procs procs =
   Net.entries procs
   |> partition_eq eq_procedure_id
   |> map (fn ps as Procedure {name, ...} :: _ => (name, map (fn Procedure {lhs, ...} => lhs) ps));
 
-fun dest_ss (Simpset ({rules, ...}, {congs, procs = simprocs, loop_tacs, solvers, ...})) =
- {simps = Net.entries rules
-    |> map (fn {name, thm, ...} => (name, thm)),
+fun dest_ss (ss as Simpset (_, {congs, procs = simprocs, loop_tacs, solvers, ...})) =
+ {simps = dest_simps ss,
   simprocs = dest_procs simprocs,
-  congs = congs |> fst |> Congtab.dest,
-  weak_congs = congs |> snd,
+  congs = dest_congs ss,
+  weak_congs = #2 congs,
   loopers = map fst loop_tacs,
   unsafe_solvers = map solver_name (#1 solvers),
   safe_solvers = map solver_name (#2 solvers)};
 
-fun dest_simps (Simpset ({rules, ...}, _)) = map #thm (Net.entries rules);
-
 
 (* empty *)
 
diff -r 552cdee5cd43 -r 29734511c661 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Aug 14 13:51:36 2024 +0200
+++ b/src/Pure/simplifier.ML	Wed Aug 14 15:30:29 2024 +0200
@@ -28,6 +28,8 @@
 signature SIMPLIFIER =
 sig
   include BASIC_SIMPLIFIER
+  val dest_simps: simpset -> (Thm_Name.T * thm) list
+  val dest_congs: simpset -> (cong_name * thm) list
   val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic
   val attrib: (thm -> Proof.context -> Proof.context) -> attribute
   val simp_add: attribute