--- a/src/Pure/library.ML Tue Mar 10 13:23:35 1998 +0100
+++ b/src/Pure/library.ML Tue Mar 10 13:24:11 1998 +0100
@@ -76,6 +76,7 @@
val length: 'a list -> int
val take: int * 'a list -> 'a list
val drop: int * 'a list -> 'a list
+ val dropwhile: ('a -> bool) -> 'a list -> 'a list
val nth_elem: int * 'a list -> 'a
val last_elem: 'a list -> 'a
val split_last: 'a list -> 'a list * 'a
@@ -424,6 +425,9 @@
| drop (n, x :: xs) =
if n > 0 then drop (n - 1, xs) else x :: xs;
+fun dropwhile P [] = []
+ | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;
+
(*return nth element of a list, where 0 designates the first element;
raise EXCEPTION if list too short*)
fun nth_elem NL =