summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Thu, 31 Aug 2006 10:17:19 +0200 | |

changeset 20443 | 84a624a8f773 |

parent 20442 | 04621ea9440e |

child 20444 | 6c5e38a73db0 |

Empty is better than Match

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