Replaced blast by fast in proof of parts_singleton, since blast looped
because of the new encoding of sets.

--- 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 *}

--- a/src/HOL/Auth/Message.thy	Wed May 07 10:57:19 2008 +0200
+++ b/src/HOL/Auth/Message.thy	Wed May 07 10:59:02 2008 +0200
@@ -181,7 +181,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 *}

--- a/src/HOL/MetisExamples/Message.thy	Wed May 07 10:57:19 2008 +0200
+++ b/src/HOL/MetisExamples/Message.thy	Wed May 07 10:59:02 2008 +0200
@@ -181,7 +181,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}"
 apply (erule parts.induct)
-apply blast+
+apply fast+
 done
 
 

--- a/src/HOL/SET-Protocol/MessageSET.thy	Wed May 07 10:57:19 2008 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy	Wed May 07 10:59:02 2008 +0200
@@ -225,7 +225,7 @@
 
 (*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*}