src/Pure/tactic.ML

       (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net
   val compose_inst_tac  : (string*string)list -> (bool*thm*int) ->
                           int -> tactic
   val compose_tac       : (bool * thm * int) -> int -> tactic
   val cut_facts_tac     : thm list -> int -> tactic
+  val cut_rules_tac     : thm list -> int -> tactic
   val cut_inst_tac      : (string*string)list -> thm -> int -> tactic
   val datac             : thm -> int -> int -> tactic
   val defer_tac         : int -> tactic
   val distinct_subgoals_tac     : tactic
   val dmatch_tac        : thm list -> int -> tactic

 (*Recognizes theorems that are not rules, but simple propositions*)
 fun is_fact rl =
     case prems_of rl of
         [] => true  |  _::_ => false;
 
-(*"Cut" all facts from theorem list into the goal as assumptions. *)
-fun cut_facts_tac ths i =
-    EVERY (map (fn th => metacut_tac th i) (filter is_fact ths));
+(*"Cut" a list of rules into the goal.  Their premises will become new
+  subgoals.*)
+fun cut_rules_tac ths i = EVERY (map (fn th => metacut_tac th i) ths);
+
+(*As above, but inserts only facts (unconditional theorems);
+  generates no additional subgoals. *)
+fun cut_facts_tac ths = cut_rules_tac  (filter is_fact ths);
 
 (*Introduce the given proposition as a lemma and subgoal*)
 fun subgoal_tac sprop =
   DETERM o res_inst_tac [("psi", sprop)] cut_rl THEN' SUBGOAL (fn (prop, _) =>
     let val concl' = Logic.strip_assums_concl prop in