# HG changeset patch
# User wenzelm
# Date 1372320521 -7200
# Node ID ef4c16887f8342ace8fca003437a9e578e92f408
# Parent  365ca7cb0d812adbb6d7b86913de6f8da6e058a4
more scalable PARALLEL_GOALS, using more elementary retrofit;
tuned signature;

diff -r 365ca7cb0d81 -r ef4c16887f83 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Jun 26 22:18:06 2013 +0200
+++ b/src/Pure/goal.ML	Thu Jun 27 10:08:41 2013 +0200
@@ -51,8 +51,6 @@
     ({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
@@ -349,22 +347,6 @@
 
 (** goal structure **)
 
-(* nested goals *)
-
-fun extract i n st =
-  (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
-   else if n = 1 then Seq.single (Thm.cprem_of st i)
-   else
-     Seq.single (Conjunction.mk_conjunction_balanced (map (Thm.cprem_of st) (i upto i + n - 1))))
-  |> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init);
-
-fun retrofit i n st' st =
-  (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 =
@@ -439,16 +421,30 @@
   in fold_rev (curry op APPEND') tacs (K no_tac) i end);
 
 
-(* parallel tacticals *)
+
+(** parallel tacticals **)
 
-(*parallel choice of single results*)
+(* parallel choice of single results *)
+
 fun PARALLEL_CHOICE tacs st =
   (case Par_List.get_some (fn tac => SINGLE tac st) tacs of
     NONE => Seq.empty
   | SOME st' => Seq.single st');
 
-(*parallel refinement of non-schematic goal by single results*)
+
+(* parallel refinement of non-schematic goal by single results *)
+
+local
+
 exception FAILED of unit;
+
+fun retrofit st' =
+  rotate_prems ~1 #>
+  Thm.bicompose {flatten = false, match = false, incremented = false}
+      (false, conclude st', Thm.nprems_of st') 1;
+
+in
+
 fun PARALLEL_GOALS tac =
   Thm.adjust_maxidx_thm ~1 #>
   (fn st =>
@@ -463,10 +459,12 @@
 
         val goals = Drule.strip_imp_prems (Thm.cprop_of st);
         val results = Par_List.map (try_tac o init) goals;
-      in ALLGOALS (fn i => retrofit i 1 (nth results (i - 1))) st end
+      in EVERY (map retrofit (rev results)) st end
       handle FAILED () => Seq.empty);
 
 end;
 
+end;
+
 structure Basic_Goal: BASIC_GOAL = Goal;
 open Basic_Goal;