diff -r 8ec47039614e -r 3dd306cb98d2 doc-src/TutorialI/Protocol/Public_lemmas.ML
--- a/doc-src/TutorialI/Protocol/Public_lemmas.ML	Tue May 08 05:30:10 2007 +0200
+++ b/doc-src/TutorialI/Protocol/Public_lemmas.ML	Tue May 08 08:21:39 2007 +0200
@@ -13,7 +13,7 @@
 
 (*** Basic properties of pubK & priK ***)
 
-AddIffs [inj_pubK RS inj_eq];
+AddIffs [inj_pubK RS @{thm inj_eq}];
 
 Goal "(priK A = priK B) = (A=B)";
 by Safe_tac;