diff -r fe5b796d6b2a -r 23b67731f4f0 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/Auth/Message.thy	Mon Mar 23 13:30:59 2015 +0100
@@ -866,7 +866,8 @@
      (EVERY 
       [  (*push in occurrences of X...*)
        (REPEAT o CHANGED)
-         (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1),
+         (Rule_Insts.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])),