tuned proof;

--- a/src/HOL/Auth/Guard/Guard_NS_Public.thy	Sun Jul 15 16:44:40 2012 +0200
+++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy	Sun Jul 15 16:53:50 2012 +0200
@@ -158,7 +158,10 @@
 apply (case_tac "NBa=NB", clarify)
 apply (drule Guard_Nonce_analz, simp+)
 apply (drule Says_imp_knows_Spy)+
-by (drule_tac A=Aa and A'=A in NB_is_uniq, auto)
+apply (drule_tac A=Aa and A'=A in NB_is_uniq)
+apply auto[1]
+apply (auto simp add: guard.No_Nonce)
+done
 
 subsection{*Agents' Authentication*}