src/HOL/Auth/Smartcard/EventSC.thy

--- a/src/HOL/Auth/Smartcard/EventSC.thy	Tue Feb 14 20:57:05 2012 +0100
+++ b/src/HOL/Auth/Smartcard/EventSC.thy	Tue Feb 14 21:19:39 2012 +0100
@@ -237,8 +237,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]
-     parts.Body [THEN revcut_rl]
+     Says_imp_knows_Spy [THEN parts.Inj, elim_format]
+     parts.Body [elim_format]