diff -r 437bd400d808 -r f9f3006a5579 src/Doc/Tutorial/Protocol/Public.thy
--- a/src/Doc/Tutorial/Protocol/Public.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/Doc/Tutorial/Protocol/Public.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -130,7 +130,7 @@
 lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs"
 apply (induct_tac "evs")
 apply (rule_tac x = 0 in exI)
-apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
+apply (simp_all (no_asm_simp) add: used_Cons split: event.split)
 apply safe
 apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
 done