diff -r 6be7cf5086ab -r 6933d20f335f src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Mon Sep 29 11:47:01 1997 +0200
@@ -230,7 +230,7 @@
 \       -->         A=A' & NA=NA' & B=B' & X=X'";
 by (etac ns_shared.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
-by (Step_tac 1);
+by Safe_tac;
 (*NS3*)
 by (ex_strip_tac 2);
 by (Blast_tac 2);
@@ -278,7 +278,7 @@
 (*Fake*) 
 by (spy_analz_tac 1);
 (*NS3, Server sub-case*) (**LEVEL 6 **)
-by (step_tac (!claset delrules [impCE]) 1);
+by (clarify_tac (!claset delrules [impCE]) 1);
 by (forward_tac [Says_imp_spies RS parts.Inj RS A_trusts_NS2] 1);
 by (assume_tac 2);
 by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj RS