# HG changeset patch
# User wenzelm
# Date 875719958 -7200
# Node ID f20b071a429a853777bb6cfa544fe7d0e7ea15d4
# Parent  d99d93d46ca530d277e2a8ad072afea4dfe80c08
added split_last;

diff -r d99d93d46ca5 -r f20b071a429a src/Pure/library.ML
--- 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)