# HG changeset patch
# User paulson
# Date 884451522 -3600
# Node ID 41fa62c229c3bafb184346fa4f96d8d37d2792e1
# Parent  53553ccda0e67b13db92b25f14936de1050dd75d
trivial tidy

diff -r 53553ccda0e6 -r 41fa62c229c3 src/HOL/Auth/NS_Public_Bad.ML
--- a/src/HOL/Auth/NS_Public_Bad.ML	Fri Jan 09 20:28:18 1998 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Sat Jan 10 17:58:42 1998 +0100
@@ -150,7 +150,7 @@
 (*Authentication for A: if she receives message 2 and has used NA
   to start a run, then B has sent message 2.*)
 goal thy 
- "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;  \
+ "!!evs. [| Says A  B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;  \
 \           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs;  \
 \           A ~: bad;  B ~: bad;  evs : ns_public |]                    \
 \        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs";