--- a/src/HOL/SET_Protocol/Message_SET.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Sun May 18 14:33:01 2025 +0000
@@ -848,7 +848,7 @@
       [  (*push in occurrences of X...*)
        (REPEAT o CHANGED)
          (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] []
-          (insert_commute RS ssubst) 1),
+          (@{thm insert_commute} RS ssubst) 1),
        (*...allowing further simplifications*)
        simp_tac ctxt 1,
        REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),