1.1 --- a/NEWS	Sat Apr 16 21:45:47 2011 +0200
     1.2 +++ b/NEWS	Sat Apr 16 22:21:34 2011 +0200
     1.3 @@ -112,6 +112,9 @@
     1.4  * Typed print translation: discontinued show_sorts argument, which is
     1.5  already available via context of "advanced" translation.
     1.6  
     1.7 +* Refined PARALLEL_GOALS tactical: degrades gracefully for schematic
     1.8 +goal states; body tactic needs to address all subgoals uniformly.
     1.9 +
    1.10  
    1.11  
    1.12  New in Isabelle2011 (January 2011)

     2.1 --- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Sat Apr 16 21:45:47 2011 +0200
     2.2 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Sat Apr 16 22:21:34 2011 +0200
     2.3 @@ -37,7 +37,7 @@
     2.4    THEN' SMT_Solver.smt_tac ctxt (Boogie_Axioms.get ctxt @ boogie_rules @ rules)
     2.5  
     2.6  fun boogie_all_tac ctxt rules =
     2.7 -  PARALLEL_GOALS (HEADGOAL (boogie_tac ctxt rules))
     2.8 +  PARALLEL_GOALS (ALLGOALS (boogie_tac ctxt rules))
     2.9  
    2.10  fun boogie_method all =
    2.11    Scan.optional Attrib.thms [] >> (fn thms => fn ctxt => METHOD (fn facts =>

     3.1 --- a/src/Pure/goal.ML	Sat Apr 16 21:45:47 2011 +0200
     3.2 +++ b/src/Pure/goal.ML	Sat Apr 16 22:21:34 2011 +0200
     3.3 @@ -344,21 +344,22 @@
     3.4  
     3.5  (*parallel refinement of non-schematic goal by single results*)
     3.6  exception FAILED of unit;
     3.7 -fun PARALLEL_GOALS tac st =
     3.8 -  let
     3.9 -    val st0 = Thm.adjust_maxidx_thm ~1 st;
    3.10 -    val _ = Thm.maxidx_of st0 >= 0 andalso
    3.11 -      raise THM ("PARALLEL_GOALS: schematic goal state", 0, [st]);
    3.12 +fun PARALLEL_GOALS tac =
    3.13 +  Thm.adjust_maxidx_thm ~1 #>
    3.14 +  (fn st =>
    3.15 +    if not (future_enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1
    3.16 +    then DETERM tac st
    3.17 +    else
    3.18 +      let
    3.19 +        fun try_tac g =
    3.20 +          (case SINGLE tac g of
    3.21 +            NONE => raise FAILED ()
    3.22 +          | SOME g' => g');
    3.23  
    3.24 -    fun try_tac g =
    3.25 -      (case SINGLE tac g of
    3.26 -        NONE => raise FAILED ()
    3.27 -      | SOME g' => g');
    3.28 -
    3.29 -    val goals = Drule.strip_imp_prems (Thm.cprop_of st0);
    3.30 -    val results = Par_List.map (try_tac o init) goals;
    3.31 -  in ALLGOALS (fn i => retrofit i 1 (nth results (i - 1))) st0 end
    3.32 -  handle FAILED () => Seq.empty;
    3.33 +        val goals = Drule.strip_imp_prems (Thm.cprop_of st);
    3.34 +        val results = Par_List.map (try_tac o init) goals;
    3.35 +      in ALLGOALS (fn i => retrofit i 1 (nth results (i - 1))) st end
    3.36 +      handle FAILED () => Seq.empty);
    3.37  
    3.38  end;
    3.39