diff -r 40b411ec05aa -r 4cd176ea28dc doc-src/TutorialI/Protocol/Message.thy
--- a/doc-src/TutorialI/Protocol/Message.thy	Wed May 07 10:57:19 2008 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy	Wed May 07 10:59:02 2008 +0200
@@ -204,7 +204,7 @@
 
 text{*WARNING: loops if H = {Y}, therefore must not be repeated!*}
 lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
-by (erule parts.induct, blast+)
+by (erule parts.induct, fast+)
 
 
 subsubsection{*Unions *}