src/Pure/library.ML
changeset 2958 7837471d2f27
parent 2806 772f6bba48a1
child 2978 83a4c4f79dcd
     1.1 --- a/src/Pure/library.ML	Wed Apr 16 18:15:32 1997 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Apr 16 18:16:02 1997 +0200
     1.3 @@ -142,6 +142,15 @@
     1.4  fun reset flag = (flag := false; false);
     1.5  fun toggle flag = (flag := not (! flag); ! flag);
     1.6  
     1.7 +fun set_ap flag value f x =
     1.8 +  let
     1.9 +    val orig_value = ! flag;
    1.10 +    fun return y = (flag := orig_value; y);
    1.11 +  in
    1.12 +    flag := value;
    1.13 +    return (f x handle exn => (return (); raise exn))
    1.14 +  end;
    1.15 +
    1.16  
    1.17  
    1.18  (** lists **)
    1.19 @@ -322,8 +331,8 @@
    1.20  
    1.21  (** integers **)
    1.22  
    1.23 -fun inc i = i := ! i + 1;
    1.24 -fun dec i = i := ! i - 1;
    1.25 +fun inc i = (i := ! i + 1; ! i);
    1.26 +fun dec i = (i := ! i - 1; ! i);
    1.27  
    1.28  
    1.29  (* lists of integers *)