--- 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 **)