src/Pure/Isar/proof.ML

   #2 (#2 (find_goal state)) |> (fn {statement, using, goal, before_qed, after_qed} =>
     Method.evaluate text ctxt using goal
     |> Seq.map (fn (meth_cases, goal') =>
       state
       |> map_goal
-          (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases ctxt goal') #>
-           Proof_Context.update_cases true meth_cases)
+          (Proof_Context.update_cases_legacy (no_goal_cases goal @ goal_cases ctxt goal') #>
+           Proof_Context.update_cases meth_cases)
           (K (statement, using, goal', before_qed, after_qed)) I));
 
 in
 
 fun refine text state = apply_method text (context_of state) state;