# HG changeset patch
# User paulson
# Date 875528023 -7200
# Node ID 3ea2f3b5e7058ce5cc10e5e244b58a5f2c9db05c
# Parent  39ee3d31cfbc66e591d32e4c4332317c8fff5c93
Step_tac -> Safe_tac

diff -r 39ee3d31cfbc -r 3ea2f3b5e705 src/HOL/IMP/Hoare.ML
--- a/src/HOL/IMP/Hoare.ML	Mon Sep 29 11:56:04 1997 +0200
+++ b/src/HOL/IMP/Hoare.ML	Mon Sep 29 12:13:43 1997 +0200
@@ -96,7 +96,7 @@
 by (ALLGOALS Simp_tac);
 by (REPEAT_FIRST Fast_tac);
 by (deepen_tac (!claset addIs [hoare.conseq]) 0 1);
-by (Step_tac 1);
+by Safe_tac;
 by (rtac hoare.conseq 1);
   by (etac thin_rl 1);
   by (Fast_tac 1);