src/Pure/library.ML
changeset 39811 0659e84bdc5f
parent 39809 dac3c3106746
child 40291 012ed4426fda
     1.1 --- a/src/Pure/library.ML	Fri Oct 01 08:25:23 2010 +0200
     1.2 +++ b/src/Pure/library.ML	Fri Oct 01 10:25:36 2010 +0200
     1.3 @@ -83,8 +83,7 @@
     1.4    val take: int -> 'a list -> 'a list
     1.5    val drop: int -> 'a list -> 'a list
     1.6    val chop: int -> 'a list -> 'a list * 'a list
     1.7 -  val take_while: ('a -> bool) -> 'a list -> 'a list
     1.8 -  val drop_while: ('a -> bool) -> 'a list -> 'a list
     1.9 +  val chop_while: ('a -> bool) -> 'a list -> 'a list * 'a list
    1.10    val nth: 'a list -> int -> 'a
    1.11    val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
    1.12    val nth_drop: int -> 'a list -> 'a list
    1.13 @@ -422,11 +421,9 @@
    1.14    | chop _ [] = ([], [])
    1.15    | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
    1.16  
    1.17 -fun drop_while P [] = []
    1.18 -  | drop_while P (ys as x :: xs) = if P x then drop_while P xs else ys;
    1.19 -
    1.20 -fun take_while P [] = []
    1.21 -  | take_while P (x :: xs) = if P x then x :: take_while P xs else [];
    1.22 +fun chop_while P [] = ([], [])
    1.23 +  | chop_while P (ys as x :: xs) =
    1.24 +      if P x then chop_while P xs |>> cons x else ([], ys);
    1.25  
    1.26  (*return nth element of a list, where 0 designates the first element;
    1.27    raise Subscript if list too short*)