# HG changeset patch
# User haftmann
# Date 1747853052 -7200
# Node ID 8a02dd7fcb5d03668dd2cc8719dafb9baa34689a
# Parent  629fa9278081ed7c166017f26a4e0bafe3d7f1a4
tuned

diff -r 629fa9278081 -r 8a02dd7fcb5d src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed May 21 22:03:53 2025 +0200
+++ b/src/HOL/HOL.thy	Wed May 21 20:44:12 2025 +0200
@@ -1917,13 +1917,10 @@
   by (simp add: ASSUMPTION_def)
 
 setup \<open>
-let
-  val asm_sol = mk_solver "ASSUMPTION" (fn ctxt =>
-    resolve_tac ctxt [@{thm ASSUMPTION_I}] THEN'
-    resolve_tac ctxt (Simplifier.prems_of ctxt))
-in
-  map_theory_simpset (fn ctxt => Simplifier.addSolver (ctxt,asm_sol))
-end
+  (map_theory_simpset o Simplifier.add_unsafe_solver) (
+    mk_solver "ASSUMPTION" (fn ctxt =>
+      resolve_tac ctxt @{thms ASSUMPTION_I} THEN'
+      resolve_tac ctxt (Simplifier.prems_of ctxt)))
 \<close>
 
 
diff -r 629fa9278081 -r 8a02dd7fcb5d src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Wed May 21 22:03:53 2025 +0200
+++ b/src/Provers/splitter.ML	Wed May 21 20:44:12 2025 +0200
@@ -438,7 +438,7 @@
 fun split_name (name, T) asm = "split " ^
   (if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T;
 
-fun gen_add_split bang split ctxt =
+fun gen_add_split bang split =
   let
     val (name, asm) = split_thm_info split
     val split0 = Thm.trim_context split
@@ -450,14 +450,14 @@
                    TRY o (SELECT_GOAL (Data.safe_tac ctxt'))
               else split_tac ctxt' [split'])
       end
-  in Simplifier.addloop (ctxt, (split_name name asm, tac)) end;
+  in Simplifier.add_loop (split_name name asm, tac) end;
 
 val add_split = gen_add_split false;
 val add_split_bang = gen_add_split true;
 
-fun del_split split ctxt =
+fun del_split split =
   let val (name, asm) = split_thm_info split
-  in Simplifier.delloop (ctxt, split_name name asm) end;
+  in Simplifier.del_loop (split_name name asm) end;
 
 
 (* attributes *)
diff -r 629fa9278081 -r 8a02dd7fcb5d src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed May 21 22:03:53 2025 +0200
+++ b/src/Pure/simplifier.ML	Wed May 21 20:44:12 2025 +0200
@@ -425,8 +425,8 @@
 
 val simplified = conv_mode -- Attrib.thms >>
   (fn (f, ths) => Thm.rule_attribute ths (fn context =>
-    f ((if null ths then I else clear_simpset)
-        (Context.proof_of context) addsimps ths)));
+    f (Context.proof_of context |>
+      (if null ths then I else clear_simpset #> add_simps ths))));
 
 end;
 
@@ -510,11 +510,11 @@
 
 val _ =
   Theory.setup
-    (method_setup [] #> Context.theory_map (map_ss (fn ctxt =>
-      empty_simpset ctxt
-      setSSolver safe_solver
-      setSolver unsafe_solver
-      |> set_subgoaler asm_simp_tac)));
+    (method_setup [] #> Context.theory_map (map_ss (
+      empty_simpset
+      #> set_safe_solver safe_solver
+      #> set_unsafe_solver unsafe_solver
+      #> set_subgoaler asm_simp_tac)));
 
 end;