src/HOL/MetisExamples/Message.thy

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