src/Pure/library.ML

--- a/src/Pure/library.ML	Thu Sep 30 09:45:18 2010 +0200
+++ b/src/Pure/library.ML	Thu Sep 30 18:37:29 2010 +0200
@@ -83,7 +83,8 @@
   val take: int -> 'a list -> 'a list
   val drop: int -> 'a list -> 'a list
   val chop: int -> 'a list -> 'a list * 'a list
-  val dropwhile: ('a -> bool) -> 'a list -> 'a list
+  val take_while: ('a -> bool) -> 'a list -> 'a list
+  val drop_while: ('a -> bool) -> 'a list -> 'a list
   val nth: 'a list -> int -> 'a
   val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
   val nth_drop: int -> 'a list -> 'a list
@@ -421,8 +422,11 @@
   | chop _ [] = ([], [])
   | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
 
-fun dropwhile P [] = []
-  | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;
+fun drop_while P [] = []
+  | drop_while P (ys as x :: xs) = if P x then drop_while P xs else ys;
+
+fun take_while P [] = []
+  | take_while P (x :: xs) = if P x then x :: take_while P xs else [];
 
 (*return nth element of a list, where 0 designates the first element;
   raise Subscript if list too short*)