src/Pure/goal.ML

--- a/src/Pure/goal.ML	Tue Aug 19 16:46:07 2014 +0200
+++ b/src/Pure/goal.ML	Tue Aug 19 17:00:44 2014 +0200
@@ -13,6 +13,7 @@
   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 =
@@ -384,6 +385,8 @@
 
 end;
 
+val PARALLEL_ALLGOALS = PARALLEL_GOALS o ALLGOALS;
+
 end;
 
 structure Basic_Goal: BASIC_GOAL = Goal;