# HG changeset patch
# User wenzelm
# Date 878830845 -3600
# Node ID fcc8b47e4c4909f41e78c4ec5ce0f28b96376e4c
# Parent  2f0df5b390e8048b658db6b0a8e7d59f98159a98
tuned;

diff -r 2f0df5b390e8 -r fcc8b47e4c49 Admin/makedist
--- a/Admin/makedist	Thu Nov 06 12:27:12 1997 +0100
+++ b/Admin/makedist	Thu Nov 06 16:40:45 1997 +0100
@@ -152,7 +152,6 @@
 
 cd $DISTBASE
 
-#FIXME sometimes doesn't work!?
 chown -R $LOGNAME:isabelle $DISTNAME
 chmod -R u+w $DISTNAME
 chmod -R g+w $DISTNAME
diff -r 2f0df5b390e8 -r fcc8b47e4c49 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Nov 06 12:27:12 1997 +0100
+++ b/src/Pure/library.ML	Thu Nov 06 16:40:45 1997 +0100
@@ -79,8 +79,8 @@
   | merge_opts merge (Some x, Some y) = Some (merge (x, y));
 
 (*handle partial functions*)
+fun can f x = (f x; true) handle _ => false;
 fun try f x = Some (f x) handle _ => None;
-fun can f x = is_some (try f x);
 
 
 
@@ -204,7 +204,7 @@
 (*  (op @) [x1, ..., xn]  ===>   x1 @ (x2 ... @ (x[n-1] @ xn))
     for n > 0, operators that associate to the right (not tail recursive)*)
 fun foldr1 f l =
-  let fun itr [x] = x                       (* FIXME [] case: elim warn (?) *)
+  let fun itr [x] = x
         | itr (x::l) = f(x, itr l)
   in  itr l  end;