src/HOL/Auth/Yahalom2.ML

--- a/src/HOL/Auth/Yahalom2.ML	Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/Yahalom2.ML	Tue Dec 16 15:17:26 1997 +0100
@@ -167,9 +167,7 @@
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
 (*Fake*) 
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
 qed_spec_mp "analz_image_freshK";
 
 goal thy