# HG changeset patch
# User paulson
# Date 875525516 -7200
# Node ID 12409b467fae9f28fb1f9ec33e50114d42a4affa
# Parent  a5b9e0ade194989758aff7ba8cc6d953b7cf0167
Step_tac -> Safe_tac

diff -r a5b9e0ade194 -r 12409b467fae src/FOL/ex/cla.ML
--- a/src/FOL/ex/cla.ML	Mon Sep 29 11:31:13 1997 +0200
+++ b/src/FOL/ex/cla.ML	Mon Sep 29 11:31:56 1997 +0200
@@ -386,7 +386,7 @@
   the type constraint ensures that x,y,z have the same type as a,b,u. *)
 goal FOL.thy "(EX x y::'a. ALL z. z=x | z=y) & P(a) & P(b) & a~=b \
 \               --> (ALL u::'a.P(u))";
-by (Step_tac 1);
+by Safe_tac;
 by (res_inst_tac [("x","a")] allE 1);
 by (assume_tac 1);
 by (res_inst_tac [("x","b")] allE 1);
@@ -431,7 +431,7 @@
 \  (ALL x. EX y. ~hates(x,y)) & \
 \  ~ agatha=butler --> \
 \  killed(?who,agatha)";
-by (Step_tac 1);
+by Safe_tac;
 by (dres_inst_tac [("x1","x")] (spec RS mp) 1);
 by (assume_tac 1);
 by (etac (spec RS exE) 1);