# HG changeset patch
# User paulson
# Date 1157012239 -7200
# Node ID 84a624a8f7733c1343ab2a2a13493bc05451a3d7
# Parent  04621ea9440eeace4c0b837fcae922bb7ef24772
Empty is better than Match

diff -r 04621ea9440e -r 84a624a8f773 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Aug 31 02:59:08 2006 +0200
+++ b/src/Pure/library.ML	Thu Aug 31 10:17:19 2006 +0200
@@ -543,10 +543,11 @@
 
 (*  (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
-        | itr (x::l) = f(x, itr l)
-  in  itr l  end;
+fun foldr1 f [] = raise Empty
+  | foldr1 f l = 
+      let fun itr [x] = x
+	    | itr (x::l) = f(x, itr l)
+      in  itr l  end;
 
 fun fold_index f =
   let