--- 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
--- 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;