tuned setmp;
authorwenzelm
Thu, 19 Jan 2006 21:22:17 +0100
changeset 18712 836520885b8f
parent 18711 cf020c54e2f5
child 18713 cf777b9788b5
tuned setmp;
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 *)