--- 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>
--- 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 *)
--- 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;