prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;

--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Mon Feb 27 15:42:07 2012 +0100
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Mon Feb 27 15:48:02 2012 +0100
@@ -93,7 +93,7 @@
     val norm_eq_th =
       simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq})
   in
-    cut_rules_tac [norm_eq_th] i
+    cut_tac norm_eq_th i
     THEN (simp_tac cring_ss i)
     THEN (simp_tac cring_ss i)
   end);

--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Feb 27 15:42:07 2012 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Feb 27 15:48:02 2012 +0100
@@ -732,7 +732,7 @@
         val tac =
             EVERY
             [rtac @{thm trans} 1, rtac map_ID_thm 2,
-             cut_facts_tac [lub_take_lemma] 1,
+             cut_tac lub_take_lemma 1,
              REPEAT (etac @{thm Pair_inject} 1), atac 1]
         val lub_take_thm = Goal.prove_global thy [] [] goal (K tac)
       in

--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Mon Feb 27 15:42:07 2012 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Mon Feb 27 15:48:02 2012 +0100
@@ -433,7 +433,7 @@
             let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites)) in
               EVERY [
                 simp_tac (HOL_ss addsimps [hd prems]) 1,
-                cut_facts_tac [nchotomy''] 1,
+                cut_tac nchotomy'' 1,
                 REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1),
                 REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)]
             end)

--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Feb 27 15:42:07 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Feb 27 15:48:02 2012 +0100
@@ -437,7 +437,7 @@
         val prems = prems0 |> map normalize_literal
                            |> distinct Term.aconv_untyped
         val goal = Logic.list_implies (prems, concl)
-        val tac = cut_rules_tac [th] 1
+        val tac = cut_tac th 1
                   THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]}
                   THEN ALLGOALS assume_tac
       in
@@ -730,7 +730,7 @@
                        cat_lines (map string_for_subst_info substs))
 *)
       fun cut_and_ex_tac axiom =
-        cut_rules_tac [axiom] 1
+        cut_tac axiom 1
         THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
       fun rotation_for_subgoal i =
         find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs

--- a/src/HOL/Tools/inductive.ML	Mon Feb 27 15:42:07 2012 +0100
+++ b/src/HOL/Tools/inductive.ML	Mon Feb 27 15:48:02 2012 +0100
@@ -432,7 +432,7 @@
       in
         (Skip_Proof.prove ctxt'' [] prems P
           (fn {prems, ...} => EVERY
-            [cut_facts_tac [hd prems] 1,
+            [cut_tac (hd prems) 1,
              rewrite_goals_tac rec_preds_defs,
              dtac (unfold RS iffD1) 1,
              REPEAT (FIRSTGOAL (eresolve_tac rules1)),

--- a/src/HOL/Tools/inductive_realizer.ML	Mon Feb 27 15:42:07 2012 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Mon Feb 27 15:48:02 2012 +0100
@@ -456,7 +456,7 @@
         val rews = map mk_meta_eq case_thms;
         val thm = Goal.prove_global thy []
           (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY
-          [cut_facts_tac [hd prems] 1,
+          [cut_tac (hd prems) 1,
            etac elimR 1,
            ALLGOALS (asm_simp_tac HOL_basic_ss),
            rewrite_goals_tac rews,

--- a/src/HOL/Tools/record.ML	Mon Feb 27 15:42:07 2012 +0100
+++ b/src/HOL/Tools/record.ML	Mon Feb 27 15:48:02 2012 +0100
@@ -1623,7 +1623,7 @@
       let val (assm, concl) = induct_prop in
         Skip_Proof.prove_global defs_thy [] [assm] concl
           (fn {prems, ...} =>
-            cut_rules_tac [split_meta RS Drule.equal_elim_rule2] 1 THEN
+            cut_tac (split_meta RS Drule.equal_elim_rule2) 1 THEN
             resolve_tac prems 2 THEN
             asm_simp_tac HOL_ss 1)
       end);

--- a/src/HOL/ex/Meson_Test.thy	Mon Feb 27 15:42:07 2012 +0100
+++ b/src/HOL/ex/Meson_Test.thy	Mon Feb 27 15:48:02 2012 +0100
@@ -28,7 +28,7 @@
     val nnf25 = Meson.make_nnf @{context} prem25;
     val xsko25 = Meson.skolemize @{context} nnf25;
   *}
-  apply (tactic {* cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1) *})
+  apply (tactic {* cut_tac xsko25 1 THEN REPEAT (etac exE 1) *})
   ML_val {*
     val [_, sko25] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal})));
     val clauses25 = Meson.make_clauses @{context} [sko25];   (*7 clauses*)
@@ -49,7 +49,7 @@
     val nnf26 = Meson.make_nnf @{context} prem26;
     val xsko26 = Meson.skolemize @{context} nnf26;
   *}
-  apply (tactic {* cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1) *})
+  apply (tactic {* cut_tac xsko26 1 THEN REPEAT (etac exE 1) *})
   ML_val {*
     val [_, sko26] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal})));
     val clauses26 = Meson.make_clauses @{context} [sko26];                   (*9 clauses*)
@@ -71,7 +71,7 @@
     val nnf43 = Meson.make_nnf @{context} prem43;
     val xsko43 = Meson.skolemize @{context} nnf43;
   *}
-  apply (tactic {* cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1) *})
+  apply (tactic {* cut_tac xsko43 1 THEN REPEAT (etac exE 1) *})
   ML_val {*
     val [_, sko43] = #prems (#1 (Subgoal.focus @{context} 1 (#goal @{Isar.goal})));
     val clauses43 = Meson.make_clauses @{context} [sko43];   (*6*)