--- a/doc-src/TutorialI/Protocol/Public_lemmas.ML	Fri Jul 20 19:54:03 2007 +0200
+++ b/doc-src/TutorialI/Protocol/Public_lemmas.ML	Sat Jul 21 09:14:16 2007 +0200
@@ -125,7 +125,7 @@
 			addsplits [expand_event_case])));
 by Safe_tac;
 by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
-by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
+by (ALLGOALS (blast_tac (claset() addSEs [@{thm add_leE}])));
 val lemma = result();
 
 Goal "EX N. Nonce N ~: used evs";