diff -r ac51bafd1afb -r 55358999077d src/HOL/Auth/NS_Shared.thy
--- a/src/HOL/Auth/NS_Shared.thy	Wed Feb 14 12:22:49 2001 +0100
+++ b/src/HOL/Auth/NS_Shared.thy	Wed Feb 14 13:01:02 2001 +0100
@@ -173,7 +173,7 @@
           \<or> X \<in> analz (spies evs)"
 apply (frule Says_imp_knows_Spy)
 (*mystery: why is this frule needed?*)
-apply (blast dest: cert_A_form  analz.Inj)
+apply (blast dest: cert_A_form analz.Inj)
 done
 
 (*Alternative version also provable
@@ -224,8 +224,8 @@
 apply (erule ns_shared.induct, force)
 apply (frule_tac [7] Says_Server_message_form)
 apply (erule_tac [4] Says_S_message_form [THEN disjE])
-apply (analz_freshK)
-apply (spy_analz)
+apply analz_freshK
+apply spy_analz
 done