src/HOL/Tools/Metis/metis_reconstruct.ML

       let
         val (prems0, concl) = th |> prop_of |> Logic.strip_horn
         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
         if length prems = length prems0 then
           raise METIS ("resynchronize", "Out of sync")

       val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
       val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
                        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
     in
       Goal.prove ctxt [] [] @{prop False}