# HG changeset patch
# User wenzelm
# Date 1201363719 -3600
# Node ID fa26b76d3e7e340817b52ad21adf24e70e7cce0a
# Parent  3297781f814163641c443730864c2ad42cc255ad
added surround;

diff -r 3297781f8141 -r fa26b76d3e7e src/Pure/library.ML
--- a/src/Pure/library.ML	Sat Jan 26 17:08:38 2008 +0100
+++ b/src/Pure/library.ML	Sat Jan 26 17:08:39 2008 +0100
@@ -110,6 +110,7 @@
   val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list
   val split_list: ('a * 'b) list -> 'a list * 'b list
   val separate: 'a -> 'a list -> 'a list
+  val surround: 'a -> 'a list -> 'a list
   val replicate: int -> 'a -> 'a list
   val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
   val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
@@ -535,6 +536,9 @@
 fun separate s (x :: (xs as _ :: _)) = x :: s :: separate s xs
   | separate _ xs = xs;
 
+fun surround s (x :: xs) = s :: x :: surround s xs
+  | surround s [] = [s];
+
 (*make the list [x, x, ..., x] of length n*)
 fun replicate (n: int) x =
   let fun rep (0, xs) = xs