src/HOL/Auth/Yahalom.thy

--- a/src/HOL/Auth/Yahalom.thy	Fri Oct 07 18:49:20 2005 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Fri Oct 07 20:41:10 2005 +0200
@@ -176,7 +176,7 @@
      "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}
            \<in> set evs;   evs \<in> yahalom |]
       ==> K \<notin> range shrK"
-by (erule rev_mp, erule yahalom.induct, simp_all, blast)
+by (erule rev_mp, erule yahalom.induct, simp_all)
 
 
 subsection{*Secrecy Theorems*}