method: SelectGoals;

--- a/src/Pure/Isar/proof.ML	Sat Mar 04 21:10:11 2006 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Mar 04 21:10:12 2006 +0100
@@ -303,6 +303,9 @@
       in map_context f (State (nd, node' :: nodes')) end
   | map_goal _ _ state = state;
 
+fun set_goal goal = map_goal I (fn (statement, using, _, before_qed, after_qed) =>
+  (statement, using, goal, before_qed, after_qed));
+
 fun using_facts using = map_goal I (fn (statement, _, goal, before_qed, after_qed) =>
   (statement, using, goal, before_qed, after_qed));
 
@@ -371,7 +374,7 @@
   end;
 
 fun pretty_goals main state =
-  let val (ctxt, (_, {goal, ...})) = find_goal state
+  let val (ctxt, (_, goal)) = get_goal state
   in pretty_goals_local ctxt "" (false, main) (! Display.goals_limit) goal end;
 
 
@@ -408,6 +411,17 @@
           (K (statement, using, goal', before_qed, after_qed)))
   end;
 
+fun select_goals n meth state =
+  let val goal = #2 (#2 (get_goal state)) in
+    state
+    |> Seq.lift set_goal
+      (Seq.maps (Tactic.precise_conjunction_tac 1 n) (Goal.extract 1 n goal))
+    |> Seq.maps meth
+    |> Seq.maps (fn state' => state'
+      |> Seq.lift set_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
+    |> Seq.maps (apply_method true (K Method.succeed))
+  end;
+
 fun apply_text cc text state =
   let
     val thy = theory_of state;
@@ -417,7 +431,8 @@
       | eval (Method.Then txts) = Seq.EVERY (map eval txts)
       | eval (Method.Orelse txts) = Seq.FIRST (map eval txts)
       | eval (Method.Try txt) = Seq.TRY (eval txt)
-      | eval (Method.Repeat1 txt) = Seq.REPEAT1 (eval txt);
+      | eval (Method.Repeat1 txt) = Seq.REPEAT1 (eval txt)
+      | eval (Method.SelectGoals (n, txt)) = select_goals n (eval txt);
   in eval text state end;
 
 in
@@ -443,15 +458,12 @@
       else all_tac)));
 
 fun refine_goal print_rule inner raw_rule state =
-  let val (outer, (_, {statement, using, goal, before_qed, after_qed})) = find_goal state in
+  let val (outer, (_, goal)) = get_goal state in
     raw_rule
     |> ProofContext.goal_exports inner outer
     |> Seq.maps (fn rule =>
       (print_rule outer rule;
-        goal
-        |> FINDGOAL (refine_tac rule)
-        |> Seq.map (fn goal' =>
-          map_goal I (K (statement, using, goal', before_qed, after_qed)) state)))
+        Seq.lift set_goal (FINDGOAL (refine_tac rule) goal) state))
   end;
 
 in