# HG changeset patch
# User paulson
# Date 875525822 -7200
# Node ID f33e301a89f579c39c65ef14ad78b0b70d9258ae
# Parent  034f0f5ca43fd148fcbd8124a6079a650904c8f3
Step_tac -> Safe_tac

diff -r 034f0f5ca43f -r f33e301a89f5 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Arith.ML	Mon Sep 29 11:37:02 1997 +0200
@@ -403,7 +403,7 @@
 Addsimps [diff_add_inverse2];
 
 goal Arith.thy "!!i j k::nat. i<=j ==> (j-i=k) = (j=k+i)";
-by (Step_tac 1);
+by Safe_tac;
 by (ALLGOALS Asm_simp_tac);
 qed "le_imp_diff_is_add";
 
@@ -546,7 +546,7 @@
 
 goal Arith.thy "!!k. 0<k ==> (m*k = n*k) = (m=n)";
 by (cut_facts_tac [less_linear] 1);
-by (Step_tac 1);
+by Safe_tac;
 by (assume_tac 2);
 by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
 by (ALLGOALS Asm_full_simp_tac);
diff -r 034f0f5ca43f -r f33e301a89f5 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Divides.ML	Mon Sep 29 11:37:02 1997 +0200
@@ -229,7 +229,7 @@
 goal thy "Suc(Suc(m)) mod 2 = m mod 2";
 by (subgoal_tac "m mod 2 < 2" 1);
 by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
-by (Step_tac 1);
+by Safe_tac;
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [mod_Suc])));
 qed "mod2_Suc_Suc";
 Addsimps [mod2_Suc_Suc];
@@ -390,7 +390,7 @@
 qed "dvd_imp_le";
 
 goalw thy [dvd_def] "!!k. 0<k ==> (k dvd n) = (n mod k = 0)";
-by (Step_tac 1);
+by Safe_tac;
 by (stac mult_commute 1);
 by (Asm_simp_tac 1);
 by (eres_inst_tac [("t","n")] (mod_div_equality RS subst) 1);
diff -r 034f0f5ca43f -r f33e301a89f5 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Finite.ML	Mon Sep 29 11:37:02 1997 +0200
@@ -378,7 +378,7 @@
 goal Finite.thy "!!A. finite(A) ==> inj_onto f A --> card (f `` A) = card A";
 by (etac finite_induct 1);
 by (ALLGOALS Asm_simp_tac);
-by (Step_tac 1);
+by Safe_tac;
 by (rewtac inj_onto_def);
 by (Blast_tac 1);
 by (stac card_insert_disjoint 1);
diff -r 034f0f5ca43f -r f33e301a89f5 src/HOL/Induct/Comb.ML
--- a/src/HOL/Induct/Comb.ML	Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Induct/Comb.ML	Mon Sep 29 11:37:02 1997 +0200
@@ -130,7 +130,7 @@
 goalw Comb.thy [diamond_def] "diamond parcontract";
 by (rtac (impI RS allI RS allI) 1);
 by (etac parcontract.induct 1 THEN prune_params_tac);
-by (Step_tac 1);
+by Safe_tac;
 by (ALLGOALS Blast_tac);
 qed "diamond_parcontract";
 
diff -r 034f0f5ca43f -r f33e301a89f5 src/HOL/Induct/LFilter.ML
--- a/src/HOL/Induct/LFilter.ML	Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Induct/LFilter.ML	Mon Sep 29 11:37:02 1997 +0200
@@ -187,7 +187,7 @@
 goal thy "lfilter p (lfilter p l) = lfilter p l";
 by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
 by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
-by (Step_tac 1);
+by Safe_tac;
 (*Cases: p x is true or false*)
 by (Blast_tac 1);
 by (rtac (lfilter_cases RS disjE) 1);
@@ -327,7 +327,7 @@
 goal thy "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)";
 by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
 by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
-by (Step_tac 1);
+by Safe_tac;
 by (Blast_tac 1);
 by (case_tac "lmap f l : Domain (findRel p)" 1);
 by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
diff -r 034f0f5ca43f -r f33e301a89f5 src/HOL/Induct/PropLog.ML
--- a/src/HOL/Induct/PropLog.ML	Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Induct/PropLog.ML	Mon Sep 29 11:37:02 1997 +0200
@@ -186,7 +186,7 @@
     "{} |= p ==> !t. hyps p t - hyps p t0 |- p";
 by (rtac (hyps_subset RS (hyps_finite RS finite_subset_induct)) 1);
 by (simp_tac (!simpset addsimps [sat RS sat_thms_p]) 1);
-by (Step_tac 1);
+by Safe_tac;
 (*Case hyps(p,t)-insert(#v,Y) |- p *)
 by (rtac thms_excluded_middle_rule 1);
 by (rtac (insert_Diff_same RS weaken_left) 1);
diff -r 034f0f5ca43f -r f33e301a89f5 src/HOL/MiniML/MiniML.ML
--- a/src/HOL/MiniML/MiniML.ML	Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/MiniML/MiniML.ML	Mon Sep 29 11:37:02 1997 +0200
@@ -125,7 +125,7 @@
 Addsimps [aux_plus];
 
 goal thy "!!t::typ. new_tv n t ==> {x. ? y. x = n + y} Int free_tv t = {}";
-by (step_tac (!claset) 1);
+by Safe_tac;
 by (cut_facts_tac [aux_plus] 1);
 by (dtac new_tv_le 1);
 by (assume_tac 1);
@@ -135,7 +135,7 @@
 val new_tv_Int_free_tv_empty_type = result ();
 
 goal thy "!!sch::type_scheme. new_tv n sch ==> {x. ? y. x = n + y} Int free_tv sch = {}";
-by (step_tac (!claset) 1);
+by Safe_tac;
 by (cut_facts_tac [aux_plus] 1);
 by (dtac new_tv_le 1);
 by (assume_tac 1);
diff -r 034f0f5ca43f -r f33e301a89f5 src/HOL/Subst/Subst.ML
--- a/src/HOL/Subst/Subst.ML	Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Subst/Subst.ML	Mon Sep 29 11:37:02 1997 +0200
@@ -181,7 +181,7 @@
 by (induct_tac "t" 1);
 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [sdom_iff,srange_iff])));
 by (Blast_tac 2);
-by (REPEAT (step_tac (!claset addIs [vars_var_iff RS iffD1 RS sym]) 1));
+by (safe_tac (!claset addSIs [exI, vars_var_iff RS iffD1 RS sym]));
 by (Auto_tac());
 qed_spec_mp "Var_intro";
 
diff -r 034f0f5ca43f -r f33e301a89f5 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);
diff -r 034f0f5ca43f -r f33e301a89f5 src/HOL/Subst/Unify.ML
--- a/src/HOL/Subst/Unify.ML	Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Subst/Unify.ML	Mon Sep 29 11:37:02 1997 +0200
@@ -44,7 +44,7 @@
 				 wf_inv_image, wf_lex_prod, wf_finite_psubset,
 				 wf_measure]) 1);
 (* TC *)
-by (Step_tac 1);
+by Safe_tac;
 by (simp_tac (!simpset addsimps [finite_psubset_def, finite_vars_of,
 				 lex_prod_def, measure_def, inv_image_def]) 1);
 by (rtac (monotone_vars_of RS (subset_iff_psubset_eq RS iffD1) RS disjE) 1);
diff -r 034f0f5ca43f -r f33e301a89f5 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/equalities.ML	Mon Sep 29 11:37:02 1997 +0200
@@ -634,7 +634,7 @@
 Addsimps [Pow_empty];
 
 goal Set.thy "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
-by (Step_tac 1);
+by Safe_tac;
 by (etac swap 1);
 by (res_inst_tac [("x", "x-{a}")] image_eqI 1);
 by (ALLGOALS Blast_tac);
diff -r 034f0f5ca43f -r f33e301a89f5 src/HOL/ex/Fib.ML
--- a/src/HOL/ex/Fib.ML	Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/ex/Fib.ML	Mon Sep 29 11:37:02 1997 +0200
@@ -54,7 +54,7 @@
     (asm_simp_tac (!simpset addsimps [add_mult_distrib, add_mult_distrib2, 
 				      mod_less, mod_Suc]
                             setloop split_tac[expand_if])));
-by (step_tac (!claset addSDs [mod2_neq_0]) 1);
+by (safe_tac (!claset addSDs [mod2_neq_0]));
 by (ALLGOALS
     (asm_full_simp_tac
      (!simpset addsimps (fib.rules @ add_ac @ mult_ac @
diff -r 034f0f5ca43f -r f33e301a89f5 src/HOLCF/Porder.ML
--- a/src/HOLCF/Porder.ML	Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOLCF/Porder.ML	Mon Sep 29 11:37:02 1997 +0200
@@ -68,7 +68,7 @@
 "!!F. is_chain(F) ==> is_tord(range(F))"
  (fn _ =>
         [
-        (Step_tac 1),
+        Safe_tac,
         (rtac nat_less_cases 1),
         (ALLGOALS (fast_tac (!claset addIs [refl_less, chain_mono RS mp])))]);