src/Pure/library.ML

   val split_list: ('a * 'b) list -> 'a list * 'b list
   val equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   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
   val lcm: int * int -> int
   val inc: int ref -> int

   | take_suffix pred (x :: xs) =
       (case take_suffix pred xs of
         ([], 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 **)
 
 fun gcd(x,y) =