diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/TutorialI/Protocol/Message_lemmas.ML
--- a/doc-src/TutorialI/Protocol/Message_lemmas.ML	Wed Jul 11 10:52:20 2007 +0200
+++ b/doc-src/TutorialI/Protocol/Message_lemmas.ML	Wed Jul 11 10:53:39 2007 +0200
@@ -450,7 +450,7 @@
 \              analz (insert (Crypt K X) H) \\<subseteq> \
 \              insert (Crypt K X) (analz (insert X H))";
 by (rtac subsetI 1);
-by (eres_inst_tac [("xa","x")] analz.induct 1);
+by (eres_inst_tac [("x","x")] analz.induct 1);
 by Auto_tac;
 val lemma1 = result();
 
@@ -458,7 +458,7 @@
 \              insert (Crypt K X) (analz (insert X H)) \\<subseteq> \
 \              analz (insert (Crypt K X) H)";
 by Auto_tac;
-by (eres_inst_tac [("xa","x")] analz.induct 1);
+by (eres_inst_tac [("x","x")] analz.induct 1);
 by Auto_tac;
 by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1);
 val lemma2 = result();