# HG changeset patch
# User wenzelm
# Date 1723718597 -7200
# Node ID 05b16602a683d4cbd471bf843eba7609b74fc872
# Parent  043e5fd3ce328c968678c0de1db26b71f5f9e9ba
clarified signature;

diff -r 043e5fd3ce32 -r 05b16602a683 src/Pure/Tools/simplifier_trace.ML
--- a/src/Pure/Tools/simplifier_trace.ML	Thu Aug 15 12:22:39 2024 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML	Thu Aug 15 12:43:17 2024 +0200
@@ -87,7 +87,7 @@
 
 fun add_thm_breakpoint thm context =
   let
-    val rrules = mk_rrules (Context.proof_of context) [thm]
+    val rrules = mk_rrules (Context.proof_of context) thm
   in
     map_breakpoints (apsnd (fold Item_Net.update rrules)) context
   end
diff -r 043e5fd3ce32 -r 05b16602a683 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Thu Aug 15 12:22:39 2024 +0200
+++ b/src/Pure/raw_simplifier.ML	Thu Aug 15 12:43:17 2024 +0200
@@ -17,7 +17,7 @@
   val simp_trace: bool Config.T
   type cong_name = bool * string
   type rrule
-  val mk_rrules: Proof.context -> thm list -> rrule list
+  val mk_rrules: Proof.context -> thm -> rrule list
   val eq_rrule: rrule * rrule -> bool
   type proc = Proof.context -> cterm -> thm option
   type solver
@@ -602,19 +602,20 @@
     else rrule_eq_True ctxt thm name lhs elhs rhs thm
   end;
 
-fun extract_rews ctxt sym thms =
+fun extract_rews sym ctxt thm =
   let
     val mk = #mk (get_mk_rews ctxt);
-    val mk' = if sym then fn ctxt => fn th => mk ctxt th RL [Drule.symmetric_thm] else mk;
-  in maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk' ctxt thm)) thms end;
+    val rews = mk ctxt thm;
+    val rews' = if sym then rews RL [Drule.symmetric_thm] else rews;
+  in map (rpair (Thm.get_name_hint thm)) rews' end;
 
 fun extract_safe_rrules ctxt thm =
-  maps (orient_rrule ctxt) (extract_rews ctxt false [thm]);
+  maps (orient_rrule ctxt) (extract_rews false ctxt thm);
 
 fun mk_rrules ctxt thms =
   let
-    val rews = extract_rews ctxt false thms
-    val raw_rrules = flat (map (mk_rrule ctxt) rews)
+    val rews = extract_rews false ctxt thms;
+    val raw_rrules = maps (mk_rrule ctxt) rews;
   in map mk_rrule2 raw_rrules end;
 
 
@@ -623,7 +624,7 @@
 local
 
 fun comb_simps ctxt comb mk_rrule sym thms =
-  let val rews = extract_rews ctxt sym (map (Thm.transfer' ctxt) thms);
+  let val rews = maps (extract_rews sym ctxt o Thm.transfer' ctxt) thms;
   in fold (fold comb o mk_rrule) rews ctxt end;
 
 (*