made 'flat' pervasive (again);
authorwenzelm
Tue Apr 25 22:23:04 2006 +0200 (2006-04-25)
changeset 19461d3bc9c1ff241
parent 19460 2b37469d52ad
child 19462 26d5f3bcc933
made 'flat' pervasive (again);
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue Apr 25 22:22:58 2006 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Apr 25 22:23:04 2006 +0200
     1.3 @@ -115,6 +115,7 @@
     1.4    val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
     1.5    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
     1.6    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
     1.7 +  val flat: 'a list list -> 'a list
     1.8    val unflat: 'a list list -> 'b list -> 'b list list
     1.9    val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
    1.10    val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
    1.11 @@ -287,7 +288,6 @@
    1.12    val take: int * 'a list -> 'a list
    1.13    val drop: int * 'a list -> 'a list
    1.14    val last_elem: 'a list -> 'a
    1.15 -  val flat: 'a list list -> 'a list
    1.16    val seq: ('a -> unit) -> 'a list -> unit
    1.17    val partition: ('a -> bool) -> 'a list -> 'a list * 'a list
    1.18    val mapfilter: ('a -> 'b option) -> 'a list -> 'b list
    1.19 @@ -654,17 +654,16 @@
    1.20  fun get_index f =
    1.21    let
    1.22      fun get _ [] = NONE
    1.23 -      | get i (x::xs) = 
    1.24 +      | get i (x :: xs) =
    1.25            case f x
    1.26 -           of NONE => get (i+1) xs
    1.27 +           of NONE => get (i + 1) xs
    1.28              | SOME y => SOME (i, y)
    1.29    in get 0 end;
    1.30  
    1.31  fun eq_list _ ([], []) = true
    1.32 -  | eq_list eq (x::xs, y::ys) = eq (x, y) andalso eq_list eq (xs, ys)
    1.33 +  | eq_list eq (x :: xs, y :: ys) = eq (x, y) andalso eq_list eq (xs, ys)
    1.34    | eq_list _ _ = false;
    1.35  
    1.36 -(*flatten a list of lists to a list*)
    1.37  val flat = List.concat;
    1.38  
    1.39  fun unflat (xs :: xss) ys =