src/Pure/Isar/proof.ML

   let
     val (goal_ctxt, (_, {statement, messages = _, using, goal, before_qed, after_qed})) =
       find_goal state;
     val ctxt = if current_context then context_of state else goal_ctxt;
   in
-    Method.apply method ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
+    method ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
       state
       |> map_goal
           (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #>
            Proof_Context.update_cases true meth_cases)
           (K (statement, [], using, goal', before_qed, after_qed)) I)

     val explicit_vars = fold Term.add_vars var_props [];
     val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []);
   in map (Logic.mk_term o Var) vars end;
 
 fun refine_terms n =
-  refine (Method.Basic (K (RAW_METHOD
-    (K (HEADGOAL (PRECISE_CONJUNCTS n
-      (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI))))))))))
+  refine (Method.Basic (K (NO_CASES o
+    K (HEADGOAL (PRECISE_CONJUNCTS n
+      (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))))
   #> Seq.hd;
 
 in
 
 fun generic_goal prepp kind before_qed after_qed raw_propp state =