Empty is better than Match
authorpaulson
Thu Aug 31 10:17:19 2006 +0200 (2006-08-31)
changeset 2044384a624a8f773
parent 20442 04621ea9440e
child 20444 6c5e38a73db0
Empty is better than Match
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Aug 31 02:59:08 2006 +0200
     1.2 +++ b/src/Pure/library.ML	Thu Aug 31 10:17:19 2006 +0200
     1.3 @@ -543,10 +543,11 @@
     1.4  
     1.5  (*  (op @) [x1, ..., xn]  ===>   x1 @ (x2 ... @ (x[n-1] @ xn))
     1.6      for n > 0, operators that associate to the right (not tail recursive)*)
     1.7 -fun foldr1 f l =
     1.8 -  let fun itr [x] = x
     1.9 -        | itr (x::l) = f(x, itr l)
    1.10 -  in  itr l  end;
    1.11 +fun foldr1 f [] = raise Empty
    1.12 +  | foldr1 f l = 
    1.13 +      let fun itr [x] = x
    1.14 +	    | itr (x::l) = f(x, itr l)
    1.15 +      in  itr l  end;
    1.16  
    1.17  fun fold_index f =
    1.18    let