PARALLEL_GOALS: proper scope for exception FAILED, with dummy argument to prevent its interpretation as variable;
authorwenzelm
Wed Sep 30 22:26:47 2009 +0200 (2009-09-30)
changeset 32788a65deb8f9434
parent 32787 4271aab3aa4a
child 32789 d89327de0b3c
PARALLEL_GOALS: proper scope for exception FAILED, with dummy argument to prevent its interpretation as variable;
src/Pure/goal.ML
     1.1 --- a/src/Pure/goal.ML	Wed Sep 30 22:26:25 2009 +0200
     1.2 +++ b/src/Pure/goal.ML	Wed Sep 30 22:26:47 2009 +0200
     1.3 @@ -300,22 +300,22 @@
     1.4    | SOME st' => Seq.single st');
     1.5  
     1.6  (*parallel refinement of non-schematic goal by single results*)
     1.7 +exception FAILED of unit;
     1.8  fun PARALLEL_GOALS tac st =
     1.9    let
    1.10      val st0 = Thm.adjust_maxidx_thm ~1 st;
    1.11      val _ = Thm.maxidx_of st0 >= 0 andalso
    1.12        raise THM ("PARALLEL_GOALS: schematic goal state", 0, [st]);
    1.13  
    1.14 -    exception FAILED;
    1.15      fun try_tac g =
    1.16        (case SINGLE tac g of
    1.17 -        NONE => raise FAILED
    1.18 +        NONE => raise FAILED ()
    1.19        | SOME g' => g');
    1.20  
    1.21      val goals = Drule.strip_imp_prems (Thm.cprop_of st0);
    1.22      val results = Par_List.map (try_tac o init) goals;
    1.23    in ALLGOALS (fn i => retrofit i 1 (nth results (i - 1))) st0 end
    1.24 -  handle FAILED => Seq.empty;
    1.25 +  handle FAILED () => Seq.empty;
    1.26  
    1.27  end;
    1.28