move legacy simplifier interfaces into separate file

--- a/src/FOL/IFOL.thy	Thu May 22 19:59:43 2025 +0200
+++ b/src/FOL/IFOL.thy	Sat May 24 09:06:26 2025 +0200
@@ -9,6 +9,7 @@
   abbrevs "?<" = "\<exists>\<^sub>\<le>\<^sub>1"
 begin
 
+ML_file \<open>~~/src/Tools/simp_legacy.ML\<close>
 ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
 ML_file \<open>~~/src/Provers/splitter.ML\<close>
 ML_file \<open>~~/src/Provers/hypsubst.ML\<close>

--- a/src/FOLP/IFOLP.thy	Thu May 22 19:59:43 2025 +0200
+++ b/src/FOLP/IFOLP.thy	Sat May 24 09:06:26 2025 +0200
@@ -9,6 +9,7 @@
 imports Pure
 begin
 
+ML_file \<open>~~/src/Tools/simp_legacy.ML\<close>
 ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
 
 setup Pure_Thy.old_appl_syntax_setup

--- a/src/HOL/HOL.thy	Thu May 22 19:59:43 2025 +0200
+++ b/src/HOL/HOL.thy	Sat May 24 09:06:26 2025 +0200
@@ -13,6 +13,7 @@
 abbrevs "?<" = "\<exists>\<^sub>\<le>\<^sub>1"
 begin
 
+ML_file \<open>~~/src/Tools/simp_legacy.ML\<close>
 ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
 ML_file \<open>~~/src/Tools/try.ML\<close>
 ML_file \<open>~~/src/Tools/quickcheck.ML\<close>

--- a/src/Pure/raw_simplifier.ML	Thu May 22 19:59:43 2025 +0200
+++ b/src/Pure/raw_simplifier.ML	Sat May 24 09:06:26 2025 +0200
@@ -4,11 +4,6 @@
 Higher-order Simplification.
 *)
 
-infix 4
-  addsimps delsimps addsimprocs delsimprocs
-  setloop addloop delloop
-  setSSolver addSSolver setSolver addSolver;
-
 signature BASIC_RAW_SIMPLIFIER =
 sig
   val simp_depth_limit: int Config.T
@@ -38,17 +33,6 @@
   val map_theory_simpset: (Proof.context -> Proof.context) -> theory -> theory
   val empty_simpset: Proof.context -> Proof.context
   val clear_simpset: Proof.context -> Proof.context
-  val addsimps: Proof.context * thm list -> Proof.context
-  val delsimps: Proof.context * thm list -> Proof.context
-  val addsimprocs: Proof.context * simproc list -> Proof.context
-  val delsimprocs: Proof.context * simproc list -> Proof.context
-  val setloop: Proof.context * (Proof.context -> int -> tactic) -> Proof.context
-  val addloop: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context
-  val delloop: Proof.context * string -> Proof.context
-  val setSSolver: Proof.context * solver -> Proof.context
-  val addSSolver: Proof.context * solver -> Proof.context
-  val setSolver: Proof.context * solver -> Proof.context
-  val addSolver: Proof.context * solver -> Proof.context
 
   val rewrite_rule: Proof.context -> thm list -> thm -> thm
   val rewrite_goals_rule: Proof.context -> thm list -> thm -> thm
@@ -673,8 +657,6 @@
 fun add_flipped_simps thms ctxt =
   comb_simps insert_rrule (mk_rrule ctxt) true thms ctxt;
 
-fun ctxt addsimps thms = ctxt |> add_simps thms;
-
 fun add_simp thm = add_simps [thm];
 
 fun del_simps thms ctxt =
@@ -683,8 +665,6 @@
 fun del_simps_quiet thms ctxt =
   comb_simps (del_rrule false) (map mk_rrule2 o mk_rrule ctxt) false thms ctxt;
 
-fun ctxt delsimps thms = ctxt |> del_simps thms;
-
 fun del_simp thm = del_simps [thm];
 
 fun flip_simps thms = del_simps_quiet thms #> add_flipped_simps thms;
@@ -828,9 +808,6 @@
 val add_proc = fold add_proc1 o split_proc;
 val del_proc = fold del_proc1 o split_proc;
 
-fun ctxt addsimprocs ps = fold add_proc ps ctxt;
-fun ctxt delsimprocs ps = fold del_proc ps ctxt;
-
 end;
 
 
@@ -888,15 +865,11 @@
   map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, _, solvers) =>
    (congs, procs, mk_rews, term_ord, subgoal_tac, [("", tac)], solvers));
 
-fun ctxt setloop tac = ctxt |> set_loop tac;
-
 fun add_loop (name, tac) =
   map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
     (congs, procs, mk_rews, term_ord, subgoal_tac,
      AList.update (op =) (name, tac) loop_tacs, solvers));
 
-fun ctxt addloop tac = ctxt |> add_loop tac;
-
 fun del_loop name ctxt = ctxt |>
   map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
     (congs, procs, mk_rews, term_ord, subgoal_tac,
@@ -904,32 +877,22 @@
       else cond_warning ctxt (fn () => "No such looper in simpset: " ^ quote name);
       AList.delete (op =) name loop_tacs), solvers));
 
-fun ctxt delloop name = ctxt |> del_loop name;
-
 fun set_safe_solver solver = map_simpset2
   (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
     (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));
 
-fun ctxt setSSolver solver = ctxt |> set_safe_solver solver;
-
 fun add_safe_solver solver = map_simpset2 (fn (congs, procs, mk_rews, term_ord,
   subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, term_ord,
     subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers)));
 
-fun ctxt addSSolver solver = ctxt |> add_safe_solver solver;
-
 fun set_unsafe_solver solver = map_simpset2 (fn (congs, procs, mk_rews, term_ord,
   subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, term_ord,
     subgoal_tac, loop_tacs, ([solver], solvers)));
 
-fun ctxt setSolver solver = ctxt |> set_unsafe_solver solver;
-
 fun add_unsafe_solver solver = map_simpset2 (fn (congs, procs, mk_rews, term_ord,
   subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, term_ord,
     subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers)));
 
-fun ctxt addSolver solver = ctxt |> add_unsafe_solver solver;
-
 fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, term_ord,
   subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, term_ord,
   subgoal_tac, loop_tacs, (solvers, solvers)));

--- a/src/Sequents/Sequents.thy	Thu May 22 19:59:43 2025 +0200
+++ b/src/Sequents/Sequents.thy	Sat May 24 09:06:26 2025 +0200
@@ -10,6 +10,8 @@
 keywords "print_pack" :: diag
 begin
 
+ML_file \<open>~~/src/Tools/simp_legacy.ML\<close>
+
 setup Pure_Thy.old_appl_syntax_setup
 
 declare [[unify_trace_bound = 20, unify_search_bound = 40]]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/simp_legacy.ML	Sat May 24 09:06:26 2025 +0200
@@ -0,0 +1,33 @@
+(*  Title:      Tools/simp_legacy.ML
+
+Legacy simplifier configuration interfaces -- to be phased out eventually.
+*)
+
+infix 4
+  addsimps delsimps addsimprocs delsimprocs
+  setloop addloop delloop
+  setSSolver addSSolver setSolver addSolver;
+
+local
+
+open Simplifier
+
+in
+
+fun ctxt addsimps thms = ctxt |> add_simps thms;
+fun ctxt delsimps thms = ctxt |> del_simps thms;
+
+fun ctxt addsimprocs procs = ctxt |> fold add_proc procs;
+fun ctxt delsimprocs procs = ctxt |> fold del_proc procs;
+
+fun ctxt setloop looper = ctxt |> set_loop looper;
+fun ctxt addloop looper = ctxt |> add_loop looper;
+fun ctxt delloop looper = ctxt |> del_loop looper;
+
+fun ctxt setSSolver solver = ctxt |> set_safe_solver solver;
+fun ctxt addSSolver solver = ctxt |> add_safe_solver solver;
+
+fun ctxt setSolver solver = ctxt |> set_unsafe_solver solver;
+fun ctxt addSolver solver = ctxt |> add_unsafe_solver solver;
+
+end