src/Pure/library.ML
changeset 4181 fcc8b47e4c49
parent 4139 e1659fd7a221
child 4188 1025a27b08f9
     1.1 --- a/src/Pure/library.ML	Thu Nov 06 12:27:12 1997 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Nov 06 16:40:45 1997 +0100
     1.3 @@ -79,8 +79,8 @@
     1.4    | merge_opts merge (Some x, Some y) = Some (merge (x, y));
     1.5  
     1.6  (*handle partial functions*)
     1.7 +fun can f x = (f x; true) handle _ => false;
     1.8  fun try f x = Some (f x) handle _ => None;
     1.9 -fun can f x = is_some (try f x);
    1.10  
    1.11  
    1.12  
    1.13 @@ -204,7 +204,7 @@
    1.14  (*  (op @) [x1, ..., xn]  ===>   x1 @ (x2 ... @ (x[n-1] @ xn))
    1.15      for n > 0, operators that associate to the right (not tail recursive)*)
    1.16  fun foldr1 f l =
    1.17 -  let fun itr [x] = x                       (* FIXME [] case: elim warn (?) *)
    1.18 +  let fun itr [x] = x
    1.19          | itr (x::l) = f(x, itr l)
    1.20    in  itr l  end;
    1.21