src/Pure/library.ML
changeset 3762 f20b071a429a
parent 3699 7c30ab9e25d1
child 3832 17a20a2af8f5
     1.1 --- a/src/Pure/library.ML	Wed Oct 01 14:30:38 1997 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Oct 01 17:32:38 1997 +0200
     1.3 @@ -225,6 +225,12 @@
     1.4    | last_elem [x] = x
     1.5    | last_elem (_ :: xs) = last_elem xs;
     1.6  
     1.7 +(*rear decomposition*)
     1.8 +fun split_last [] = raise LIST "split_last"
     1.9 +  | split_last [x] = ([], x)
    1.10 +  | split_last (x :: xs) = apfst (cons x) (split_last xs);
    1.11 +
    1.12 +
    1.13  (*find the position of an element in a list*)
    1.14  fun find (x, ys) =
    1.15    let fun f (y :: ys, i) = if x = y then i else f (ys, i + 1)