# HG changeset patch
# User wenzelm
# Date 1302985294 -7200
# Node ID 244911efd2750dffacffa462fe8b9db6f3597f6f
# Parent  167e8ba0f4b1a9281e030e3b763cee79c53e2072
refined PARALLEL_GOALS;

diff -r 167e8ba0f4b1 -r 244911efd275 NEWS
--- a/NEWS	Sat Apr 16 21:45:47 2011 +0200
+++ b/NEWS	Sat Apr 16 22:21:34 2011 +0200
@@ -112,6 +112,9 @@
 * Typed print translation: discontinued show_sorts argument, which is
 already available via context of "advanced" translation.
 
+* Refined PARALLEL_GOALS tactical: degrades gracefully for schematic
+goal states; body tactic needs to address all subgoals uniformly.
+
 
 
 New in Isabelle2011 (January 2011)
diff -r 167e8ba0f4b1 -r 244911efd275 src/HOL/Boogie/Tools/boogie_tactics.ML
--- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Sat Apr 16 21:45:47 2011 +0200
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Sat Apr 16 22:21:34 2011 +0200
@@ -37,7 +37,7 @@
   THEN' SMT_Solver.smt_tac ctxt (Boogie_Axioms.get ctxt @ boogie_rules @ rules)
 
 fun boogie_all_tac ctxt rules =
-  PARALLEL_GOALS (HEADGOAL (boogie_tac ctxt rules))
+  PARALLEL_GOALS (ALLGOALS (boogie_tac ctxt rules))
 
 fun boogie_method all =
   Scan.optional Attrib.thms [] >> (fn thms => fn ctxt => METHOD (fn facts =>
diff -r 167e8ba0f4b1 -r 244911efd275 src/Pure/goal.ML
--- 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;