src/HOL/Auth/Recur.ML
changeset 3451 d10f100676d8
parent 3207 fe79ad367d77
child 3465 e85c24717cad
--- a/src/HOL/Auth/Recur.ML	Thu Jun 19 11:28:55 1997 +0200
+++ b/src/HOL/Auth/Recur.ML	Thu Jun 19 11:31:14 1997 +0200
@@ -268,8 +268,8 @@
      (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
 (*Base*)
 by (Blast_tac 1);
-(*RA4, RA2, Fake*) 
-by (REPEAT (spy_analz_tac 1));
+(*Fake*) 
+by (spy_analz_tac 1);
 val raw_analz_image_freshK = result();
 qed_spec_mp "analz_image_freshK";