src/HOL/Subst/Unifier.ML

--- a/src/HOL/Subst/Unifier.ML	Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Subst/Unifier.ML	Mon Sep 29 11:37:02 1997 +0200
@@ -55,7 +55,7 @@
      "!!v. ~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t";
 by (simp_tac(!simpset addsimps [MGU_iff, Unifier_def, MoreGeneral_def]
 	              delsimps [subst_Var]) 1);
-by (Step_tac 1);
+by Safe_tac;
 by (rtac exI 1);
 by (etac subst 1 THEN rtac (Cons_trivial RS subst_sym) 1);
 by (etac ssubst_subst2 1);