tuned;
authorwenzelm
Thu Nov 06 16:40:45 1997 +0100 (1997-11-06)
changeset 4181fcc8b47e4c49
parent 4180 2f0df5b390e8
child 4182 47067b5db7ef
tuned;
Admin/makedist
src/Pure/library.ML
     1.1 --- a/Admin/makedist	Thu Nov 06 12:27:12 1997 +0100
     1.2 +++ b/Admin/makedist	Thu Nov 06 16:40:45 1997 +0100
     1.3 @@ -152,7 +152,6 @@
     1.4  
     1.5  cd $DISTBASE
     1.6  
     1.7 -#FIXME sometimes doesn't work!?
     1.8  chown -R $LOGNAME:isabelle $DISTNAME
     1.9  chmod -R u+w $DISTNAME
    1.10  chmod -R g+w $DISTNAME
     2.1 --- a/src/Pure/library.ML	Thu Nov 06 12:27:12 1997 +0100
     2.2 +++ b/src/Pure/library.ML	Thu Nov 06 16:40:45 1997 +0100
     2.3 @@ -79,8 +79,8 @@
     2.4    | merge_opts merge (Some x, Some y) = Some (merge (x, y));
     2.5  
     2.6  (*handle partial functions*)
     2.7 +fun can f x = (f x; true) handle _ => false;
     2.8  fun try f x = Some (f x) handle _ => None;
     2.9 -fun can f x = is_some (try f x);
    2.10  
    2.11  
    2.12  
    2.13 @@ -204,7 +204,7 @@
    2.14  (*  (op @) [x1, ..., xn]  ===>   x1 @ (x2 ... @ (x[n-1] @ xn))
    2.15      for n > 0, operators that associate to the right (not tail recursive)*)
    2.16  fun foldr1 f l =
    2.17 -  let fun itr [x] = x                       (* FIXME [] case: elim warn (?) *)
    2.18 +  let fun itr [x] = x
    2.19          | itr (x::l) = f(x, itr l)
    2.20    in  itr l  end;
    2.21