diff -r b0331b0d33a3 -r 2289a3869c88 doc-src/TutorialI/Protocol/Event.thy
--- a/doc-src/TutorialI/Protocol/Event.thy	Tue Feb 14 20:57:05 2012 +0100
+++ b/doc-src/TutorialI/Protocol/Event.thy	Tue Feb 14 21:19:39 2012 +0100
@@ -139,8 +139,8 @@
 text{*Elimination rules: derive contradictions from old Says events containing
   items known to be fresh*}
 lemmas knows_Spy_partsEs =
-     Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
-     parts.Body [THEN revcut_rl, standard]
+     Says_imp_knows_Spy [THEN parts.Inj, elim_format] 
+     parts.Body [elim_format]
 
 lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]