# HG changeset patch
# User haftmann
# Date 1748521107 -7200
# Node ID cf86e095a439b68c736fbe2e9f8f6e2dcf60a3bf
# Parent  6dc902967236b5d5e972350fce7530f021eef892
tuned

diff -r 6dc902967236 -r cf86e095a439 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Thu May 29 14:17:09 2025 +0200
+++ b/src/Pure/raw_simplifier.ML	Thu May 29 14:18:27 2025 +0200
@@ -625,9 +625,33 @@
 local
 
 fun comb_simps comb mk_rrule sym thms ctxt =
-  let val rews = maps (fn thm => #1 (extract_rews sym (Thm.transfer' ctxt thm) ctxt)) thms;
+  let
+    val rews = thms
+      |> maps (fn thm => #1 (extract_rews sym (Thm.transfer' ctxt thm) ctxt));
   in fold (fold comb o mk_rrule) rews ctxt end;
 
+in
+
+fun add_simps thms ctxt =
+  comb_simps insert_rrule (mk_rrule ctxt) false thms ctxt;
+
+fun add_flipped_simps thms ctxt =
+  comb_simps insert_rrule (mk_rrule ctxt) true thms ctxt;
+
+fun add_simp thm = add_simps [thm];
+
+fun del_simps thms ctxt =
+  comb_simps (del_rrule true) (map mk_rrule2 o mk_rrule ctxt) false thms ctxt;
+
+fun del_simps_quiet thms ctxt =
+  comb_simps (del_rrule false) (map mk_rrule2 o mk_rrule ctxt) false thms ctxt;
+
+fun del_simp thm = del_simps [thm];
+
+fun flip_simps thms = del_simps_quiet thms #> add_flipped_simps thms;
+
+fun flip_simp thm = flip_simps [thm];
+
 (*
 This code checks if the symetric version of a rule is already in the simpset.
 However, the variable names in the two versions of the rule may differ.
@@ -649,25 +673,7 @@
     val Simpset({rules, ...},_) = simpset_of ctxt
   in exists (present ctxt rules) rrules end
 *)
-in
 
-fun add_simps thms ctxt =
-  comb_simps insert_rrule (mk_rrule ctxt) false thms ctxt;
-
-fun add_flipped_simps thms ctxt =
-  comb_simps insert_rrule (mk_rrule ctxt) true thms ctxt;
-
-fun add_simp thm = add_simps [thm];
-
-fun del_simps thms ctxt =
-  comb_simps (del_rrule true) (map mk_rrule2 o mk_rrule ctxt) false thms ctxt;
-
-fun del_simps_quiet thms ctxt =
-  comb_simps (del_rrule false) (map mk_rrule2 o mk_rrule ctxt) false thms ctxt;
-
-fun del_simp thm = del_simps [thm];
-
-fun flip_simps thms = del_simps_quiet thms #> add_flipped_simps thms;
 (*
 with check for presence of symmetric version:
   if sym_present ctxt [thm]
@@ -675,8 +681,6 @@
   else ctxt addsimps [thm];
 *)
 
-fun flip_simp thm = flip_simps [thm];
-
 end;
 
 fun init_simpset thms ctxt = ctxt