eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
eliminated obsolete alias rewtac for rewrite_goals_tac;

--- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Nov 18 18:25:10 2008 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Nov 18 18:25:42 2008 +0100
@@ -214,7 +214,7 @@
           (map cert insts)) induct;
         val (tac, _) = Library.foldl mk_unique_tac
           (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
-              THEN rewtac (mk_meta_eq choice_eq), rec_intrs),
+              THEN rewrite_goals_tac [mk_meta_eq choice_eq], rec_intrs),
             descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
 
       in split_conj_thm (SkipProof.prove_global thy1 [] []

--- a/src/HOL/Tools/inductive_package.ML	Tue Nov 18 18:25:10 2008 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Tue Nov 18 18:25:42 2008 +0100
@@ -33,9 +33,9 @@
   val inductive_forall_name: string
   val inductive_forall_def: thm
   val rulify: thm -> thm
-  val inductive_cases: (Attrib.binding * string list) list -> Proof.context ->
+  val inductive_cases: (Attrib.binding * string list) list -> local_theory ->
     thm list list * local_theory
-  val inductive_cases_i: (Attrib.binding * term list) list -> Proof.context ->
+  val inductive_cases_i: (Attrib.binding * term list) list -> local_theory ->
     thm list list * local_theory
   type inductive_flags
   val add_inductive_i:
@@ -753,9 +753,10 @@
        if coind then
          singleton (ProofContext.export
            (snd (Variable.add_fixes (map (fst o dest_Free) params) ctxt1)) ctxt1)
-           (rotate_prems ~1 (ObjectLogic.rulify (rule_by_tactic
-             (rewrite_tac [le_fun_def, le_bool_def, sup_fun_eq, sup_bool_eq] THEN
-               fold_tac rec_preds_defs) (mono RS (fp_def RS def_coinduct)))))
+           (rotate_prems ~1 (ObjectLogic.rulify
+             (fold_rule rec_preds_defs
+               (rewrite_rule [le_fun_def, le_bool_def, sup_fun_eq, sup_bool_eq]
+                (mono RS (fp_def RS def_coinduct))))))
        else
          prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
            rec_preds_defs ctxt1);

--- a/src/HOLCF/IOA/NTP/Impl.thy	Tue Nov 18 18:25:10 2008 +0100
+++ b/src/HOLCF/IOA/NTP/Impl.thy	Tue Nov 18 18:25:42 2008 +0100
@@ -220,7 +220,7 @@
     (@{thm raw_inv1} RS @{thm invariantE})] 1 *})
 
   apply (tactic "tac2 1")
-  apply (tactic {* fold_tac [rewrite_rule [@{thm Packet.hdr_def}]
+  apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}]
     (@{thm Impl.hdr_sum_def})] *})
   apply arith
 
@@ -238,7 +238,7 @@
                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
   apply (intro strip)
   apply (erule conjE)+
-  apply (tactic {* fold_tac  [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
+  apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
   apply simp
 
   done

--- a/src/Provers/splitter.ML	Tue Nov 18 18:25:10 2008 +0100
+++ b/src/Provers/splitter.ML	Tue Nov 18 18:25:42 2008 +0100
@@ -105,7 +105,7 @@
 val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
   [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
   (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
-  (fn {prems = [prem], ...} => rewtac prem THEN rtac reflexive_thm 1)
+  (fn {prems, ...} => rewrite_goals_tac prems THEN rtac reflexive_thm 1)
 
 val trlift = lift RS transitive_thm;
 val _ $ (P $ _) $ _ = concl_of trlift;

--- a/src/Pure/meta_simplifier.ML	Tue Nov 18 18:25:10 2008 +0100
+++ b/src/Pure/meta_simplifier.ML	Tue Nov 18 18:25:42 2008 +0100
@@ -79,12 +79,10 @@
   val rewrite_rule: thm list -> thm -> thm
   val rewrite_goals_rule: thm list -> thm -> thm
   val rewrite_goals_tac: thm list -> tactic
-  val rewrite_tac: thm list -> tactic
   val rewrite_goal_tac: thm list -> int -> tactic
   val rewtac: thm -> tactic
   val prune_params_tac: tactic
   val fold_rule: thm list -> thm -> thm
-  val fold_tac: thm list -> tactic
   val fold_goals_tac: thm list -> tactic
 end;
 
@@ -1285,14 +1283,11 @@
 
 (** meta-rewriting tactics **)
 
-(*Rewrite throughout proof state. *)
-fun rewrite_tac defs = PRIMITIVE (rewrite_rule defs);
-
-(*Rewrite subgoals only, not main goal. *)
+(*Rewrite all subgoals*)
 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
 fun rewtac def = rewrite_goals_tac [def];
 
-(*Rewrite subgoal i only.*)
+(*Rewrite one subgoal*)
 fun asm_rewrite_goal_tac mode prover_tac ss i thm =
   if 0 < i andalso i <= Thm.nprems_of thm then
     Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm)
@@ -1329,7 +1324,6 @@
 val rev_defs = sort_lhs_depths o map symmetric;
 
 fun fold_rule defs = fold rewrite_rule (rev_defs defs);
-fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
 fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
 
 

--- a/src/ZF/Tools/datatype_package.ML	Tue Nov 18 18:25:10 2008 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Tue Nov 18 18:25:42 2008 +0100
@@ -291,7 +291,7 @@
       (Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg))
       (*Proves a single case equation.  Could use simp_tac, but it's slower!*)
       (fn _ => EVERY
-        [rewtac con_def,
+        [rewrite_goals_tac [con_def],
          rtac case_trans 1,
          REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]);
 

--- a/src/ZF/Tools/inductive_package.ML	Tue Nov 18 18:25:10 2008 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Tue Nov 18 18:25:42 2008 +0100
@@ -262,7 +262,7 @@
                 ORELSE' bound_hyp_subst_tac))
       THEN prune_params_tac
           (*Mutual recursion: collapse references to Part(D,h)*)
-      THEN fold_tac part_rec_defs;
+      THEN (PRIMITIVE (fold_rule part_rec_defs));
 
   (*Elimination*)
   val elim = rule_by_tactic basic_elim_tac