# HG changeset patch
# User wenzelm
# Date 1254342407 -7200
# Node ID a65deb8f9434571f1a4000449ea9d1052045d583
# Parent  4271aab3aa4acb967518b12fec3dd9dc107a83bf
PARALLEL_GOALS: proper scope for exception FAILED, with dummy argument to prevent its interpretation as variable;

diff -r 4271aab3aa4a -r a65deb8f9434 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Sep 30 22:26:25 2009 +0200
+++ b/src/Pure/goal.ML	Wed Sep 30 22:26:47 2009 +0200
@@ -300,22 +300,22 @@
   | SOME st' => Seq.single st');
 
 (*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]);
 
-    exception FAILED;
     fun try_tac g =
       (case SINGLE tac g of
-        NONE => raise FAILED
+        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;
+  handle FAILED () => Seq.empty;
 
 end;