diff -r 8f0b2daa7eaa -r d93ead9ac6df src/HOL/TLA/Action.thy
--- a/src/HOL/TLA/Action.thy	Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/TLA/Action.thy	Thu Jun 12 12:44:47 2025 +0200
@@ -260,7 +260,7 @@
 *)
 fun action_simp_tac ctxt intros elims =
     asm_full_simp_tac
-         (ctxt setloop (fn _ => (resolve_tac ctxt ((map (action_use ctxt) intros)
+         (ctxt |> Simplifier.set_loop (fn _ => (resolve_tac ctxt ((map (action_use ctxt) intros)
                                     @ [refl,impI,conjI,@{thm actionI},@{thm intI},allI]))
                       ORELSE' (eresolve_tac ctxt ((map (action_use ctxt) elims)
                                              @ [conjE,disjE,exE]))));