author | wenzelm |
Wed, 01 Oct 1997 17:32:38 +0200 | |
changeset 3762 | f20b071a429a |
parent 3761 | d99d93d46ca5 |
child 3763 | 31ec17820f49 |
--- a/src/Pure/library.ML Wed Oct 01 14:30:38 1997 +0200 +++ b/src/Pure/library.ML Wed Oct 01 17:32:38 1997 +0200 @@ -225,6 +225,12 @@ | last_elem [x] = x | last_elem (_ :: xs) = last_elem xs; +(*rear decomposition*) +fun split_last [] = raise LIST "split_last" + | split_last [x] = ([], x) + | split_last (x :: xs) = apfst (cons x) (split_last xs); + + (*find the position of an element in a list*) fun find (x, ys) = let fun f (y :: ys, i) = if x = y then i else f (ys, i + 1)