diff -r 8ec47039614e -r 3dd306cb98d2 doc-src/TutorialI/Protocol/Message_lemmas.ML
--- a/doc-src/TutorialI/Protocol/Message_lemmas.ML	Tue May 08 05:30:10 2007 +0200
+++ b/doc-src/TutorialI/Protocol/Message_lemmas.ML	Tue May 08 08:21:39 2007 +0200
@@ -849,7 +849,7 @@
   concerns  Crypt K X \\<notin> Key`shrK`bad  and cannot be proved by rewriting
   alone.*)
 fun prove_simple_subgoals_tac i = 
-    force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
+    force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN
     ALLGOALS Asm_simp_tac;
 
 fun Fake_parts_insert_tac i =