src/Pure/goal.ML
changeset 42370 244911efd275
parent 42360 da8817d01e7c
child 42371 5900f06b4198
     1.1 --- a/src/Pure/goal.ML	Sat Apr 16 21:45:47 2011 +0200
     1.2 +++ b/src/Pure/goal.ML	Sat Apr 16 22:21:34 2011 +0200
     1.3 @@ -344,21 +344,22 @@
     1.4  
     1.5  (*parallel refinement of non-schematic goal by single results*)
     1.6  exception FAILED of unit;
     1.7 -fun PARALLEL_GOALS tac st =
     1.8 -  let
     1.9 -    val st0 = Thm.adjust_maxidx_thm ~1 st;
    1.10 -    val _ = Thm.maxidx_of st0 >= 0 andalso
    1.11 -      raise THM ("PARALLEL_GOALS: schematic goal state", 0, [st]);
    1.12 +fun PARALLEL_GOALS tac =
    1.13 +  Thm.adjust_maxidx_thm ~1 #>
    1.14 +  (fn st =>
    1.15 +    if not (future_enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1
    1.16 +    then DETERM tac st
    1.17 +    else
    1.18 +      let
    1.19 +        fun try_tac g =
    1.20 +          (case SINGLE tac g of
    1.21 +            NONE => raise FAILED ()
    1.22 +          | SOME g' => g');
    1.23  
    1.24 -    fun try_tac g =
    1.25 -      (case SINGLE tac g of
    1.26 -        NONE => raise FAILED ()
    1.27 -      | SOME g' => g');
    1.28 -
    1.29 -    val goals = Drule.strip_imp_prems (Thm.cprop_of st0);
    1.30 -    val results = Par_List.map (try_tac o init) goals;
    1.31 -  in ALLGOALS (fn i => retrofit i 1 (nth results (i - 1))) st0 end
    1.32 -  handle FAILED () => Seq.empty;
    1.33 +        val goals = Drule.strip_imp_prems (Thm.cprop_of st);
    1.34 +        val results = Par_List.map (try_tac o init) goals;
    1.35 +      in ALLGOALS (fn i => retrofit i 1 (nth results (i - 1))) st end
    1.36 +      handle FAILED () => Seq.empty);
    1.37  
    1.38  end;
    1.39