# HG changeset patch
# User wenzelm
# Date 1519036148 -3600
# Node ID 0cae317eda7b659414aa82b622aa1489ed87211d
# Parent  11b390e971f6bc0e20a7c96d93f1b95896ec61e8
misc tuning and clarification;

diff -r 11b390e971f6 -r 0cae317eda7b src/Pure/par_tactical.ML
--- a/src/Pure/par_tactical.ML	Mon Feb 19 11:13:25 2018 +0100
+++ b/src/Pure/par_tactical.ML	Mon Feb 19 11:29:08 2018 +0100
@@ -41,20 +41,22 @@
 in
 
 fun PARALLEL_GOALS tac st =
-  if not (Multithreading.enabled ()) orelse Thm.nprems_of st <= 1 then DETERM tac st
-  else
-    let val subgoals = map (Thm.adjust_maxidx_cterm ~1) (Drule.strip_imp_prems (Thm.cprop_of st)) in
-      if exists (fn sg => Thm.maxidx_of_cterm sg >= 0) subgoals then DETERM tac st
-      else
-        let
-          fun try_tac g =
-            (case SINGLE tac g of
-              NONE => raise FAILED ()
-            | SOME g' => g');
-          val results = Par_List.map (try_tac o Goal.init) subgoals;
-        in EVERY (map retrofit (rev results)) st end
-        handle FAILED () => Seq.empty
-    end;
+  let
+    val goals =
+      Drule.strip_imp_prems (Thm.cprop_of st)
+      |> map (Thm.adjust_maxidx_cterm ~1);
+  in
+    if Multithreading.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
+  end;
 
 end;