1.1 --- a/src/Pure/library.ML	Fri Oct 04 15:57:32 2002 +0200
     1.2 +++ b/src/Pure/library.ML	Mon Oct 07 19:01:51 2002 +0200
     1.3 @@ -90,6 +90,7 @@
     1.4    val length: 'a list -> int
     1.5    val take: int * 'a list -> 'a list
     1.6    val drop: int * 'a list -> 'a list
     1.7 +  val splitAt: int * 'a list -> 'a list * 'a list
     1.8    val dropwhile: ('a -> bool) -> 'a list -> 'a list
     1.9    val nth_elem: int * 'a list -> 'a
    1.10    val map_nth_elem: int -> ('a -> 'a) -> 'a list -> 'a list
    1.11 @@ -507,6 +508,11 @@
    1.12    | drop (n, x :: xs) =
    1.13        if n > 0 then drop (n - 1, xs) else x :: xs;
    1.14  
    1.15 +fun splitAt(n,[]) = ([],[])
    1.16 +  | splitAt(n,xs as x::ys) =
    1.17 +      if n>0 then let val (ps,qs) = splitAt(n-1,ys) in (x::ps,qs) end
    1.18 +      else ([],xs)
    1.19 +
    1.20  fun dropwhile P [] = []
    1.21    | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;
    1.22  
    1.23 @@ -532,15 +538,10 @@
    1.24    | split_last (x :: xs) = apfst (cons x) (split_last xs);
    1.25  
    1.26  (*update nth element*)
    1.27 -fun nth_update x (n, xs) =
    1.28 -  let
    1.29 -    val prfx = take (n, xs);
    1.30 -    val sffx = drop (n, xs);
    1.31 -  in
    1.32 -    (case sffx of
    1.33 -      [] => raise LIST "nth_update"
    1.34 -    | _ :: sffx' => prfx @ (x :: sffx'))
    1.35 -  end;
    1.36 +fun nth_update x n_xs =
    1.37 +    (case splitAt n_xs of
    1.38 +      (_,[]) => raise LIST "nth_update"
    1.39 +    | (prfx, _ :: sffx') => prfx @ (x :: sffx'))
    1.40  
    1.41  (*find the position of an element in a list*)
    1.42  fun find_index pred =
    1.43 @@ -566,7 +567,8 @@
    1.44  fun flat (ls: 'c list list) : 'c list = foldr (op @) (ls, []);
    1.45  
    1.46  fun unflat (xs :: xss) ys =
    1.47 -      let val n = length xs in take (n, ys) :: unflat xss (drop (n, ys)) end
    1.48 +      let val (ps,qs) = splitAt(length xs,ys)
    1.49 +      in ps :: unflat xss qs end
    1.50    | unflat [] [] = []
    1.51    | unflat _ _ = raise LIST "unflat";
    1.52  
    1.53 @@ -1032,10 +1034,8 @@
    1.54  fun fold_bal f [x] = x
    1.55    | fold_bal f [] = raise Balance
    1.56    | fold_bal f xs =
    1.57 -      let val k = length xs div 2
    1.58 -      in  f (fold_bal f (take(k, xs)),
    1.59 -             fold_bal f (drop(k, xs)))
    1.60 -      end;
    1.61 +      let val (ps,qs) = splitAt(length xs div 2, xs)
    1.62 +      in  f (fold_bal f ps, fold_bal f qs)  end;
    1.63  
    1.64  (*construct something of the form f(...g(...(x)...)) for balanced access*)
    1.65  fun access_bal (f, g, x) n i =