src/HOL/TLA/Action.thy

    should plug in only "very safe" rules that can be applied blindly.
    Note that it applies whatever simplifications are currently active.
 *)
 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]))));
 \<close>