diff -r 414e04d7c2d6 -r 8df171ccdbd8 src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Wed Sep 17 16:37:27 1997 +0200
+++ b/src/HOL/Auth/Yahalom.ML	Wed Sep 17 16:37:40 1997 +0200
@@ -164,7 +164,7 @@
 by (etac yahalom.induct 1);
 by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
-by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
+by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
 (*Fake*) 
 by (spy_analz_tac 2);
@@ -383,14 +383,13 @@
 (*For Oops, simplification proves NBa~=NB.  By Says_Server_KeyWithNonce,
   we get (~ KeyWithNonce K NB evsa); then simplification can apply the
   induction hypothesis with KK = {K}.*)
-by (ALLGOALS  (*22 seconds*)
+by (ALLGOALS  (*17 seconds*)
     (asm_simp_tac 
      (analz_image_freshK_ss addsimps
-        ([all_conj_distrib, analz_image_freshK,
-	  KeyWithNonce_Says, fresh_not_KeyWithNonce, 
-	  imp_disj_not1,  (*Moves NBa~=NB to the front*)
-	  Says_Server_KeyWithNonce] 
-	 @ pushes))));
+        [all_conj_distrib, analz_image_freshK,
+	 KeyWithNonce_Says, fresh_not_KeyWithNonce, 
+	 imp_disj_not1,			      (*Moves NBa~=NB to the front*)
+	 Says_Server_KeyWithNonce])));
 (*Base*)
 by (Blast_tac 1);
 (*Fake*) 
@@ -506,7 +505,7 @@
 by analz_sees_tac;
 by (ALLGOALS
     (asm_simp_tac 
-     (!simpset addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes)
+     (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
                setloop split_tac [expand_if])));
 (*Prove YM3 by showing that no NB can also be an NA*)
 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]