src/Tools/simp_legacy.ML

--- a/src/Tools/simp_legacy.ML	Thu Jun 12 08:03:05 2025 +0200
+++ b/src/Tools/simp_legacy.ML	Thu Jun 12 12:44:47 2025 +0200
@@ -3,31 +3,10 @@
 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;
+infix 4 addsimps delsimps addsimprocs delsimprocs;
 
-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 addsimps thms = ctxt |> Simplifier.add_simps thms;
+fun ctxt delsimps thms = ctxt |> Simplifier.del_simps thms;
 
-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
+fun ctxt addsimprocs procs = ctxt |> fold Simplifier.add_proc procs;
+fun ctxt delsimprocs procs = ctxt |> fold Simplifier.del_proc procs;