# HG changeset patch
# User wenzelm
# Date 1372276103 -7200
# Node ID 210bca64b894816ce7670780b86928d325b2023f
# Parent  c3b4b74a54fd68e23af5a005c504709737a19a9e
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
even less intrusive PREFER_GOAL (without structural goal marker), e.g. relevant for generic_simp_tac;
adapted ZF proof that broke for unknown reasons (potentially slight change of Drule.size_of_thm);

diff -r c3b4b74a54fd -r 210bca64b894 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jun 26 18:38:03 2013 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Jun 26 21:48:23 2013 +0200
@@ -402,10 +402,10 @@
   ALLGOALS Goal.conjunction_tac (#2 (#2 (get_goal state)))
   |> Seq.maps (fn goal =>
     state
-    |> Seq.lift provide_goal (Goal.extract 1 n goal |> Seq.maps (Goal.conjunction_tac 1))
+    |> Seq.lift provide_goal ((PRIMITIVE (Goal.restrict 1 n) THEN Goal.conjunction_tac 1) goal)
     |> Seq.maps meth
     |> Seq.maps (fn state' => state'
-      |> Seq.lift provide_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
+      |> Seq.lift provide_goal (PRIMITIVE (Goal.unrestrict 1) (#2 (#2 (get_goal state')))))
     |> Seq.maps (apply_method true (K Method.succeed)));
 
 fun apply_text cc text state =
diff -r c3b4b74a54fd -r 210bca64b894 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Jun 26 18:38:03 2013 +0200
+++ b/src/Pure/goal.ML	Wed Jun 26 21:48:23 2013 +0200
@@ -9,6 +9,7 @@
   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
@@ -52,6 +53,8 @@
     ({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
@@ -361,9 +364,25 @@
   |> 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 *)
diff -r c3b4b74a54fd -r 210bca64b894 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Jun 26 18:38:03 2013 +0200
+++ b/src/Pure/simplifier.ML	Wed Jun 26 21:48:23 2013 +0200
@@ -220,7 +220,7 @@
     fun simp_loop_tac i =
       Raw_Simplifier.generic_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ctxt i THEN
       (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
-  in SELECT_GOAL (simp_loop_tac 1) end;
+  in PREFER_GOAL (simp_loop_tac 1) end;
 
 local
 
diff -r c3b4b74a54fd -r 210bca64b894 src/ZF/Constructible/Relative.thy
--- a/src/ZF/Constructible/Relative.thy	Wed Jun 26 18:38:03 2013 +0200
+++ b/src/ZF/Constructible/Relative.thy	Wed Jun 26 21:48:23 2013 +0200
@@ -753,8 +753,6 @@
      "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
       ==> M(RepFun(A,f))"
 apply (simp add: RepFun_def)
-apply (rule strong_replacement_closed)
-apply (auto dest: transM  simp add: univalent_def)
 done
 
 lemma Replace_conj_eq: "{y . x \<in> A, x\<in>A & y=f(x)} = {y . x\<in>A, y=f(x)}"