diff -r d35fca99b3be -r 7837471d2f27 src/Pure/library.ML --- a/src/Pure/library.ML Wed Apr 16 18:15:32 1997 +0200 +++ b/src/Pure/library.ML Wed Apr 16 18:16:02 1997 +0200 @@ -142,6 +142,15 @@ fun reset flag = (flag := false; false); fun toggle flag = (flag := not (! flag); ! flag); +fun set_ap 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; + (** lists **) @@ -322,8 +331,8 @@ (** integers **) -fun inc i = i := ! i + 1; -fun dec i = i := ! i - 1; +fun inc i = (i := ! i + 1; ! i); +fun dec i = (i := ! i - 1; ! i); (* lists of integers *)