Deleted spurious reference to Spy_not_see_NB, which by chance was defined
in Yahalom.ML\!

--- a/src/HOL/Auth/NS_Public_Bad.ML	Tue Jun 17 09:01:56 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Wed Jun 18 15:19:37 1997 +0200
@@ -123,8 +123,8 @@
 by (step_tac (!claset addSIs [analz_insertI]) 1);
 by (ex_strip_tac 1);
 by (blast_tac (!claset delrules [conjI]
-                      addSDs [impOfSubs Fake_parts_insert]
-                      addDs  [impOfSubs analz_subset_parts]) 1);
+                       addSDs [impOfSubs Fake_parts_insert]
+                       addDs  [impOfSubs analz_subset_parts]) 1);
 val lemma = result();
 
 goal thy 
@@ -256,8 +256,7 @@
 by (step_tac (!claset delrules [allI]) 1);
 by (Blast_tac 5);
 (*NS3*)
-by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj,
-			      Spy_not_see_NB, unique_NB]) 4);
+by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj, unique_NB]) 4);
 (*NS2*)
 by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]