src/Pure/library.ML

--- a/src/Pure/library.ML	Thu Aug 23 12:55:23 2012 +0200
+++ b/src/Pure/library.ML	Thu Aug 23 13:03:29 2012 +0200
@@ -74,7 +74,6 @@
   val take: int -> 'a list -> 'a list
   val drop: int -> 'a list -> 'a list
   val chop: int -> 'a list -> 'a list * 'a list
-  val chop_while: ('a -> bool) -> 'a list -> 'a list * 'a list
   val chop_groups: int -> 'a list -> 'a list list
   val nth: 'a list -> int -> 'a
   val nth_list: 'a list list -> int -> 'a list
@@ -413,10 +412,6 @@
   | chop _ [] = ([], [])
   | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
 
-fun chop_while P [] = ([], [])
-  | chop_while P (ys as x :: xs) =
-      if P x then chop_while P xs |>> cons x else ([], ys);
-
 fun chop_groups n list =
   (case chop (Int.max (n, 1)) list of
     ([], _) => []