# HG changeset patch
# User paulson
# Date 905441113 -7200
# Node ID 30cb9d2800148b1a488e33a82d01cfe18b18225f
# Parent  b38332431a8c311dbf9d7ec0c758d7b49333acaf
patch to stop failing proof

diff -r b38332431a8c -r 30cb9d280014 src/HOL/Auth/NS_Shared.ML
--- 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);