diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/SET_Protocol/Cardholder_Registration.thy
--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy	Wed Feb 12 08:37:06 2014 +0100
@@ -671,6 +671,7 @@
 lemma N_fresh_not_KeyCryptNonce:
      "\<forall>C. DK \<noteq> priEK C ==> Nonce N \<notin> used evs --> ~ KeyCryptNonce DK N evs"
 apply (induct_tac "evs")
+apply (rename_tac [2] a evs')
 apply (case_tac [2] "a")
 apply (auto simp add: parts_insert2)
 done