--- a/src/HOL/SET_Protocol/Message_SET.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy Fri Mar 20 14:48:04 2015 +0100
@@ -871,7 +871,7 @@
(EVERY
[ (*push in occurrences of X...*)
(REPEAT o CHANGED)
- (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])),