# HG changeset patch
# User wenzelm
# Date 1137702137 -3600
# Node ID 836520885b8f812e29579725201e2b29ebf932f4
# Parent  cf020c54e2f57457b89408a5ee3accd9dab4d035
tuned setmp;

diff -r cf020c54e2f5 -r 836520885b8f src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Jan 19 21:22:16 2006 +0100
+++ b/src/Pure/library.ML	Thu Jan 19 21:22:17 2006 +0100
@@ -471,15 +471,14 @@
 
 fun change r f = r := f (! r);
 
-(*temporarily set flag, handling exceptions*)
+(*temporarily set flag during execution*)
 fun setmp flag value f x =
   let
     val orig_value = ! flag;
-    fun return y = (flag := orig_value; y);
-  in
-    flag := value;
-    return (f x handle exn => (return (); raise exn))
-  end;
+    val _ = flag := value;
+    val result = capture f x;
+    val _ = flag := orig_value;
+  in release result end;
 
 
 (* conditional execution *)