diff -r 9a75e9772761 -r 4127c1d910f1 doc-src/TutorialI/Protocol/Message_lemmas.ML
--- a/doc-src/TutorialI/Protocol/Message_lemmas.ML	Fri Jul 20 19:54:03 2007 +0200
+++ b/doc-src/TutorialI/Protocol/Message_lemmas.ML	Sat Jul 21 09:14:16 2007 +0200
@@ -330,10 +330,10 @@
 by (induct_tac "msg" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2])));
 (*MPair case: blast_tac works out the necessary sum itself!*)
-by (blast_tac (claset() addSEs [add_leE]) 2);
+by (blast_tac (claset() addSEs [@{thm add_leE}]) 2);
 (*Nonce case*)
 by (res_inst_tac [("x","N + Suc nat")] exI 1);
-by (auto_tac (claset() addSEs [add_leE], simpset()));
+by (auto_tac (claset() addSEs [@{thm add_leE}], simpset()));
 qed "msg_Nonce_supply";