src/HOL/Auth/Shared.ML
changeset 3730 6933d20f335f
parent 3708 56facaebf3e3
child 3908 4f19a40a9343
--- a/src/HOL/Auth/Shared.ML	Mon Sep 29 11:46:33 1997 +0200
+++ b/src/HOL/Auth/Shared.ML	Mon Sep 29 11:47:01 1997 +0200
@@ -112,7 +112,7 @@
 by (ALLGOALS (asm_simp_tac
 	      (!simpset addsimps [used_Cons]
 			setloop split_tac [expand_event_case, expand_if])));
-by (Step_tac 1);
+by Safe_tac;
 by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
 by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
 val lemma = result();