diff -r f059876ef1d3 -r dd9a51255855 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Nov 20 20:55:50 2001 +0100
+++ b/src/Pure/library.ML	Tue Nov 20 20:56:13 2001 +0100
@@ -119,6 +119,8 @@
   val prefix: ''a list * ''a list -> bool
   val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
   val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
+  val prefixes1: 'a list -> 'a list list
+  val suffixes1: 'a list -> 'a list list
 
   (*integers*)
   val gcd: int * int -> int
@@ -665,6 +667,11 @@
         ([], sffx) => if pred x then ([], x :: sffx) else ([x], sffx)
       | (prfx, sffx) => (x :: prfx, sffx));
 
+fun prefixes1 [] = []
+  | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
+
+fun suffixes1 xs = map rev (prefixes1 (rev xs));
+
 
 
 (** integers **)