diff -r 8f0b2daa7eaa -r d93ead9ac6df src/HOL/TLA/Memory/MemoryImplementation.thy --- a/src/HOL/TLA/Memory/MemoryImplementation.thy Thu Jun 12 08:03:05 2025 +0200 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Thu Jun 12 12:44:47 2025 +0200 @@ -231,7 +231,7 @@ else K no_tac); \ -setup \map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver)\ +setup \map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_safe_solver fast_solver)\ ML \val temp_elim = make_elim oo temp_use\