src/Doc/Tutorial/Protocol/Message.thy

--- a/src/Doc/Tutorial/Protocol/Message.thy	Thu Sep 11 18:54:36 2014 +0200
+++ b/src/Doc/Tutorial/Protocol/Message.thy	Thu Sep 11 18:54:36 2014 +0200
@@ -334,6 +334,7 @@
  txt{*MPair case: blast works out the necessary sum itself!*}
  prefer 2 apply auto apply (blast elim!: add_leE)
 txt{*Nonce case*}
+apply (rename_tac nat)
 apply (rule_tac x = "N + Suc nat" in exI, auto) 
 done
 (*>*)