src/HOL/Auth/OtwayRees_Bad.ML
changeset 4422 21238c9d363e
parent 4091 771b1f6422a8
child 4449 df30e75f670f
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Tue Dec 16 15:17:26 1997 +0100
@@ -176,9 +176,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";