--- a/src/FOL/simpdata.ML Thu Jun 12 08:03:05 2025 +0200
+++ b/src/FOL/simpdata.ML Thu Jun 12 12:44:47 2025 +0200
@@ -125,8 +125,8 @@
(*No simprules, but basic infastructure for simplification*)
val FOL_basic_ss =
empty_simpset \<^context>
- setSSolver (mk_solver "FOL safe" safe_solver)
- setSolver (mk_solver "FOL unsafe" unsafe_solver)
+ |> Simplifier.set_safe_solver (mk_solver "FOL safe" safe_solver)
+ |> Simplifier.set_unsafe_solver (mk_solver "FOL unsafe" unsafe_solver)
|> Simplifier.set_subgoaler asm_simp_tac
|> Simplifier.set_mksimps (mksimps mksimps_pairs)
|> Simplifier.set_mkcong mk_meta_cong