patch to stop failing proof

--- a/src/HOL/Auth/NS_Shared.ML	Thu Sep 10 17:23:51 1998 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Thu Sep 10 17:25:13 1998 +0200
@@ -252,7 +252,7 @@
 by (assume_tac 2);
 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS
 			       Crypt_Spy_analz_bad]) 1);
-by (blast_tac (claset() addDs [unique_session_keys]) 1);
+by (blast_tac (claset() addSDs [unique_session_keys]) 1);
 val lemma = result() RS mp RS mp RSN(2,rev_notE);