src/Pure/library.ML
changeset 48902 44a6967240b7
parent 48271 b28defd0b5a5
child 50637 81d6fe75ea5b
     1.1 --- a/src/Pure/library.ML	Thu Aug 23 12:55:23 2012 +0200
     1.2 +++ b/src/Pure/library.ML	Thu Aug 23 13:03:29 2012 +0200
     1.3 @@ -74,7 +74,6 @@
     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 chop_while: ('a -> bool) -> 'a list -> 'a list * 'a list
     1.8    val chop_groups: int -> 'a list -> 'a list list
     1.9    val nth: 'a list -> int -> 'a
    1.10    val nth_list: 'a list list -> int -> 'a list
    1.11 @@ -413,10 +412,6 @@
    1.12    | chop _ [] = ([], [])
    1.13    | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
    1.14  
    1.15 -fun chop_while P [] = ([], [])
    1.16 -  | chop_while P (ys as x :: xs) =
    1.17 -      if P x then chop_while P xs |>> cons x else ([], ys);
    1.18 -
    1.19  fun chop_groups n list =
    1.20    (case chop (Int.max (n, 1)) list of
    1.21      ([], _) => []