diff -r d2bf12727c8a -r f2f42f9fa09d doc-src/TutorialI/Protocol/Message.thy
--- a/doc-src/TutorialI/Protocol/Message.thy	Mon Jun 16 17:56:08 2008 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy	Mon Jun 16 22:13:39 2008 +0200
@@ -864,7 +864,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,