--- 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 *)