src/Pure/library.ML
changeset 25980 fa26b76d3e7e
parent 25943 d431d65346a1
child 26079 a58cc0cf4176
     1.1 --- a/src/Pure/library.ML	Sat Jan 26 17:08:38 2008 +0100
     1.2 +++ b/src/Pure/library.ML	Sat Jan 26 17:08:39 2008 +0100
     1.3 @@ -110,6 +110,7 @@
     1.4    val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list
     1.5    val split_list: ('a * 'b) list -> 'a list * 'b list
     1.6    val separate: 'a -> 'a list -> 'a list
     1.7 +  val surround: 'a -> 'a list -> 'a list
     1.8    val replicate: int -> 'a -> 'a list
     1.9    val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
    1.10    val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
    1.11 @@ -535,6 +536,9 @@
    1.12  fun separate s (x :: (xs as _ :: _)) = x :: s :: separate s xs
    1.13    | separate _ xs = xs;
    1.14  
    1.15 +fun surround s (x :: xs) = s :: x :: surround s xs
    1.16 +  | surround s [] = [s];
    1.17 +
    1.18  (*make the list [x, x, ..., x] of length n*)
    1.19  fun replicate (n: int) x =
    1.20    let fun rep (0, xs) = xs