# HG changeset patch
# User wenzelm
# Date 1342364030 -7200
# Node ID 865610355ef376e1b1d93aaebd6193dfcd1d2ad1
# Parent  65ed3b2b315757bccd1c4de7072a2531fe855250
tuned proof;

diff -r 65ed3b2b3157 -r 865610355ef3 src/HOL/Auth/Guard/Guard_NS_Public.thy
--- 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*}