diff -r 19c277ea65ae -r e549969355b2 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jun 24 23:03:55 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Jun 25 12:10:07 2015 +0200
@@ -422,8 +422,8 @@
     |> 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