src/Pure/library.ML

   val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
   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
   val find_index: ('a -> bool) -> 'a list -> int
   val find_index_eq: ''a -> ''a list -> int

 (*drop the first n elements from a list*)
 fun drop (n, []) = []
   | 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 =
   (case drop NL of
     [] => raise LIST "nth_elem"