diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/SET-Protocol/MessageSET.thy
--- a/src/HOL/SET-Protocol/MessageSET.thy	Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy	Mon Jun 16 22:13:39 2008 +0200
@@ -880,7 +880,7 @@
      (EVERY
       [  (*push in occurrences of X...*)
        (REPEAT o CHANGED)
-           (RuleInsts.res_inst_tac (Simplifier.the_context ss)
+           (res_inst_tac (Simplifier.the_context ss)
              [(("x", 1), "X")] (insert_commute RS ssubst) 1),
        (*...allowing further simplifications*)
        simp_tac ss 1,