src/Pure/Isar/proof.ML

   | map_goal f g (State (nd, node :: nodes)) =
       let val State (node', nodes') = map_goal f g (State (node, nodes))
       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));
 
 local
   fun find i state =

      else if mode = Chain then pretty_facts "picking " context facts
      else prt_goal (try find_goal state))
   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;
 
 
 
 (** proof steps **)

           (ProofContext.add_cases false (no_goal_cases goal @ goal_cases goal') #>
            ProofContext.add_cases true meth_cases)
           (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;
 
     fun eval (Method.Basic m) = apply_method cc m
       | eval (Method.Source src) = apply_method cc (Method.method thy src)
       | 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
 
 val refine = apply_text true;

       if can Logic.unprotect (Logic.strip_assums_concl goal) then
         Tactic.etac Drule.protectI i
       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
 
 fun refine_goals print_rule inner raw_rules =