src/HOL/SET_Protocol/Message_SET.thy

   DETERM
    (SELECT_GOAL
      (EVERY
       [  (*push in occurrences of X...*)
        (REPEAT o CHANGED)
-           (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
+           (res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1),
        (*...allowing further simplifications*)
        simp_tac ctxt 1,
        REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),
        DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i);
 *}