src/FOL/simpdata.ML
changeset 82695 d93ead9ac6df
parent 82643 f1c14af17591
--- 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