src/HOL/Auth/NS_Public_Bad.thy

--- a/src/HOL/Auth/NS_Public_Bad.thy	Fri Feb 16 08:27:17 2001 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.thy	Fri Feb 16 13:25:08 2001 +0100
@@ -202,7 +202,7 @@
 apply (erule ns_public.induct, simp_all)
 apply spy_analz
 (*NS1: by freshness*)
-apply (blast)
+apply blast
 (*NS2: by freshness and unicity of NB*)
 apply (blast intro: no_nonce_NS1_NS2)
 (*NS3: unicity of NB identifies A and NA, but not B*)