# HG changeset patch
# User wenzelm
# Date 1408464664 -7200
# Node ID 987c848d509b9d1400728fbd10d1a7a66903af17
# Parent  aa72531f972f1fdcc4dd30a913cc07baf8007bf9
clarified modules;

diff -r aa72531f972f -r 987c848d509b src/Pure/ROOT
--- a/src/Pure/ROOT	Tue Aug 19 17:00:44 2014 +0200
+++ b/src/Pure/ROOT	Tue Aug 19 18:11:04 2014 +0200
@@ -233,6 +233,7 @@
     "morphism.ML"
     "name.ML"
     "net.ML"
+    "par_tactical.ML"
     "pattern.ML"
     "primitive_defs.ML"
     "proofterm.ML"
diff -r aa72531f972f -r 987c848d509b src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Aug 19 17:00:44 2014 +0200
+++ b/src/Pure/ROOT.ML	Tue Aug 19 18:11:04 2014 +0200
@@ -255,6 +255,7 @@
 (** bootstrap phase 2: towards Pure.thy and final ML toplevel setup *)
 
 (*basic proof engine*)
+use "par_tactical.ML";
 use "Isar/proof_display.ML";
 use "Isar/attrib.ML";
 use "Isar/context_rules.ML";
diff -r aa72531f972f -r 987c848d509b src/Pure/goal.ML
--- a/src/Pure/goal.ML	Tue Aug 19 17:00:44 2014 +0200
+++ b/src/Pure/goal.ML	Tue Aug 19 18:11:04 2014 +0200
@@ -11,9 +11,6 @@
   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
-  val PARALLEL_ALLGOALS: (int -> tactic) -> tactic
 end;
 
 signature GOAL =
@@ -341,52 +338,6 @@
       etac (Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)) THEN_ALL_NEW assume_tac);
   in fold_rev (curry op APPEND') tacs (K no_tac) i end);
 
-
-
-(** parallel tacticals **)
-
-(* 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 *)
-
-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 =>
-    if not (Multithreading.enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1
-    then DETERM tac st
-    else
-      let
-        fun try_tac g =
-          (case SINGLE tac g of
-            NONE => raise FAILED ()
-          | SOME g' => g');
-
-        val goals = Drule.strip_imp_prems (Thm.cprop_of st);
-        val results = Par_List.map (try_tac o init) goals;
-      in EVERY (map retrofit (rev results)) st end
-      handle FAILED () => Seq.empty);
-
-end;
-
-val PARALLEL_ALLGOALS = PARALLEL_GOALS o ALLGOALS;
-
 end;
 
 structure Basic_Goal: BASIC_GOAL = Goal;
diff -r aa72531f972f -r 987c848d509b src/Pure/par_tactical.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/par_tactical.ML	Tue Aug 19 18:11:04 2014 +0200
@@ -0,0 +1,68 @@
+(*  Title:      Pure/par_tactical.ML
+    Author:     Makarius
+
+Parallel tacticals.
+*)
+
+signature BASIC_PAR_TACTICAL =
+sig
+  val PARALLEL_CHOICE: tactic list -> tactic
+  val PARALLEL_GOALS: tactic -> tactic
+  val PARALLEL_ALLGOALS: (int -> tactic) -> tactic
+end;
+
+signature PAR_TACTICAL =
+sig
+  include BASIC_PAR_TACTICAL
+end;
+
+structure Par_Tactical: PAR_TACTICAL =
+struct
+
+(* 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 *)
+
+local
+
+exception FAILED of unit;
+
+fun retrofit st' =
+  rotate_prems ~1 #>
+  Thm.bicompose {flatten = false, match = false, incremented = false}
+      (false, Goal.conclude st', Thm.nprems_of st') 1;
+
+in
+
+fun PARALLEL_GOALS tac =
+  Thm.adjust_maxidx_thm ~1 #>
+  (fn st =>
+    if not (Multithreading.enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1
+    then DETERM tac st
+    else
+      let
+        fun try_tac g =
+          (case SINGLE tac g of
+            NONE => raise FAILED ()
+          | SOME g' => g');
+
+        val goals = Drule.strip_imp_prems (Thm.cprop_of st);
+        val results = Par_List.map (try_tac o Goal.init) goals;
+      in EVERY (map retrofit (rev results)) st end
+      handle FAILED () => Seq.empty);
+
+end;
+
+val PARALLEL_ALLGOALS = PARALLEL_GOALS o ALLGOALS;
+
+end;
+
+structure Basic_Par_Tactical: BASIC_PAR_TACTICAL = Par_Tactical;
+open Basic_Par_Tactical;
+