# HG changeset patch
# User berghofe
# Date 1108482975 -3600
# Node ID accd51fdae3c27be3c13f3152152419299a837ae
# Parent  9712d41db5b8a6b2d5083ca4ecdab767d80b8321
refine now provides specific cases "goal1" ... "goaln" for addressing
subgoals of a proof state.

diff -r 9712d41db5b8 -r accd51fdae3c src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Feb 14 10:24:58 2005 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Feb 15 16:56:15 2005 +0100
@@ -465,6 +465,10 @@
   if Sign.subsig (sg, sign_of state) then state
   else raise STATE ("Bad signature of result: " ^ Sign.str_of_sg sg, state);
 
+fun mk_goals_cases st =
+  RuleCases.make true NONE (sign_of_thm st, prop_of st)
+    (map (fn i => "goal" ^ string_of_int i) (1 upto nprems_of st));
+
 fun gen_refine current_context meth_fun state =
   let
     val (goal_ctxt, (_, ((result, (facts, thm)), x))) = find_goal state;
@@ -473,7 +477,8 @@
     fun refn (thm', cases) =
       state
       |> check_sign (Thm.sign_of_thm thm')
-      |> map_goal (ProofContext.add_cases cases) (K ((result, (facts, thm')), x));
+      |> map_goal (ProofContext.add_cases (cases @ mk_goals_cases thm'))
+           (K ((result, (facts, thm')), x));
   in Seq.map refn (meth facts thm) end;
 
 in