# 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; (*