# HG changeset patch
# User wenzelm
# Date 1132684488 -3600
# Node ID 628c117800770ab5e0bf4fdeb5b05734991fe7ad
# Parent  d4cfa0fee007873ef0b1135b9eeb78e69f7dc5da
cases_tactic;

diff -r d4cfa0fee007 -r 628c11780077 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Nov 22 19:34:47 2005 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Nov 22 19:34:48 2005 +0100
@@ -386,7 +386,7 @@
 fun no_goal_cases st = map (rpair NONE) (goals st);
 
 fun goal_cases st =
-  RuleCases.make true NONE (Thm.theory_of_thm st, Thm.prop_of st) (goals st);
+  RuleCases.make true NONE (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
 
 fun check_theory thy state =
   if subthy (thy, theory_of state) then state
@@ -397,7 +397,7 @@
     val (goal_ctxt, (_, {statement, using, goal, before_qed, after_qed})) = find_goal state;
     val meth = meth_fun (if current_context then context_of state else goal_ctxt);
   in
-    Method.apply meth using goal |> Seq.map (fn (goal', meth_cases) =>
+    Method.apply meth using goal |> Seq.map (fn (meth_cases, goal') =>
       state
       |> check_theory (Thm.theory_of_thm goal')
       |> map_goal