--- a/src/Pure/goal.ML Sat Apr 16 21:45:47 2011 +0200
+++ b/src/Pure/goal.ML Sat Apr 16 22:21:34 2011 +0200
@@ -344,21 +344,22 @@
(*parallel refinement of non-schematic goal by single results*)
exception FAILED of unit;
-fun PARALLEL_GOALS tac st =
- let
- val st0 = Thm.adjust_maxidx_thm ~1 st;
- val _ = Thm.maxidx_of st0 >= 0 andalso
- raise THM ("PARALLEL_GOALS: schematic goal state", 0, [st]);
+fun PARALLEL_GOALS tac =
+ Thm.adjust_maxidx_thm ~1 #>
+ (fn st =>
+ if not (future_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');
- fun try_tac g =
- (case SINGLE tac g of
- NONE => raise FAILED ()
- | SOME g' => g');
-
- val goals = Drule.strip_imp_prems (Thm.cprop_of st0);
- val results = Par_List.map (try_tac o init) goals;
- in ALLGOALS (fn i => retrofit i 1 (nth results (i - 1))) st0 end
- handle FAILED () => Seq.empty;
+ 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
+ handle FAILED () => Seq.empty);
end;