src/Pure/goal.ML

 signature BASIC_GOAL =
 sig
   val skip_proofs: bool Unsynchronized.ref
   val parallel_proofs: int Unsynchronized.ref
   val SELECT_GOAL: tactic -> int -> tactic
+  val PREFER_GOAL: tactic -> int -> tactic
   val CONJUNCTS: tactic -> int -> tactic
   val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
   val PARALLEL_CHOICE: tactic list -> tactic
   val PARALLEL_GOALS: tactic -> tactic
 end;

     ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val prove_sorry_global: theory -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val extract: int -> int -> thm -> thm Seq.seq
   val retrofit: int -> int -> thm -> thm -> thm Seq.seq
+  val restrict: int -> int -> thm -> thm
+  val unrestrict: int -> thm -> thm
   val conjunction_tac: int -> tactic
   val precise_conjunction_tac: int -> int -> tactic
   val recover_conjunction_tac: tactic
   val norm_hhf_tac: int -> tactic
   val assume_rule_tac: Proof.context -> int -> tactic

   (if n = 1 then st
    else st |> Drule.with_subgoal i (Conjunction.uncurry_balanced n))
   |> Thm.bicompose {flatten = false, match = false, incremented = false}
       (false, conclude st', Thm.nprems_of st') i;
 
+
+(* rearrange subgoals *)
+
+fun restrict i n st =
+  if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st
+  then raise THM ("Goal.restrict", i, [st])
+  else rotate_prems (i - 1) st |> protect n;
+
+fun unrestrict i = conclude #> rotate_prems (1 - i);
+
+(*with structural marker*)
 fun SELECT_GOAL tac i st =
   if Thm.nprems_of st = 1 andalso i = 1 then tac st
-  else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st;
+  else (PRIMITIVE (restrict i 1) THEN tac THEN PRIMITIVE (unrestrict i)) st;
+
+(*without structural marker*)
+fun PREFER_GOAL tac i st =
+  if i < 1 orelse i > Thm.nprems_of st then Seq.empty
+  else (PRIMITIVE (rotate_prems (i - 1)) THEN tac THEN PRIMITIVE (rotate_prems (1 - i))) st;
 
 
 (* multiple goals *)
 
 fun precise_conjunction_tac 0 i = eq_assume_tac i