src/Pure/library.ML
changeset 18712 836520885b8f
parent 18681 3020496cff28
child 18923 34f9df073ad9
     1.1 --- a/src/Pure/library.ML	Thu Jan 19 21:22:16 2006 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Jan 19 21:22:17 2006 +0100
     1.3 @@ -471,15 +471,14 @@
     1.4  
     1.5  fun change r f = r := f (! r);
     1.6  
     1.7 -(*temporarily set flag, handling exceptions*)
     1.8 +(*temporarily set flag during execution*)
     1.9  fun setmp flag value f x =
    1.10    let
    1.11      val orig_value = ! flag;
    1.12 -    fun return y = (flag := orig_value; y);
    1.13 -  in
    1.14 -    flag := value;
    1.15 -    return (f x handle exn => (return (); raise exn))
    1.16 -  end;
    1.17 +    val _ = flag := value;
    1.18 +    val result = capture f x;
    1.19 +    val _ = flag := orig_value;
    1.20 +  in release result end;
    1.21  
    1.22  
    1.23  (* conditional execution *)