src/Pure/par_tactical.ML

--- a/src/Pure/par_tactical.ML	Tue Aug 13 10:27:21 2019 +0200
+++ b/src/Pure/par_tactical.ML	Tue Aug 13 15:34:46 2019 +0200
@@ -14,6 +14,8 @@
 signature PAR_TACTICAL =
 sig
   include BASIC_PAR_TACTICAL
+  val strip_goals: thm -> cterm list option
+  val retrofit_tac: {close: bool} -> thm list -> tactic
 end;
 
 structure Par_Tactical: PAR_TACTICAL =
@@ -29,35 +31,43 @@
 
 (* parallel refinement of non-schematic goal by single results *)
 
-local
-
-exception FAILED of unit;
-
-fun retrofit st' =
-  rotate_prems ~1 #>
-  Thm.bicompose NONE {flatten = false, match = false, incremented = false}
-      (false, Goal.conclude st', Thm.nprems_of st') 1;
-
-in
-
-fun PARALLEL_GOALS tac st =
+fun strip_goals st =
   let
     val goals =
       Drule.strip_imp_prems (Thm.cprop_of st)
       |> map (Thm.adjust_maxidx_cterm ~1);
   in
-    if Future.relevant goals andalso forall (fn g => Thm.maxidx_of_cterm g = ~1) goals then
-      let
-        fun try_goal g =
-          (case SINGLE tac (Goal.init g) of
-            NONE => raise FAILED ()
-          | SOME st' => st');
-        val results = Par_List.map try_goal goals;
-      in EVERY (map retrofit (rev results)) st
-      end handle FAILED () => Seq.empty
-    else DETERM tac st
+    if not (null goals) andalso forall (fn g => Thm.maxidx_of_cterm g = ~1) goals
+    then SOME goals else NONE
   end;
 
+local
+
+exception FAILED of unit;
+
+fun retrofit {close} st' =
+  rotate_prems ~1 #>
+  Thm.bicompose NONE {flatten = false, match = false, incremented = false}
+      (false, Goal.conclude st' |> close ? Thm.close_derivation \<^here>, Thm.nprems_of st') 1;
+
+in
+
+fun retrofit_tac close = EVERY o map (retrofit close);
+
+fun PARALLEL_GOALS tac st =
+  (case strip_goals st of
+    SOME goals =>
+      if Future.relevant goals then
+        let
+          fun try_goal g =
+            (case SINGLE tac (Goal.init g) of
+              NONE => raise FAILED ()
+            | SOME st' => st');
+          val results = Par_List.map try_goal goals;
+        in retrofit_tac {close = false} (rev results) st end handle FAILED () => Seq.empty
+      else DETERM tac st
+  | NONE => DETERM tac st);
+
 end;
 
 val PARALLEL_ALLGOALS = PARALLEL_GOALS o ALLGOALS;