# HG changeset patch
# User wenzelm
# Date 1145996584 -7200
# Node ID d3bc9c1ff2418b5260ffb7ce34c24cbd4ca00ab6
# Parent  2b37469d52adf04dbc6b8acbf2bcd2ee7072426f
made 'flat' pervasive (again);

diff -r 2b37469d52ad -r d3bc9c1ff241 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Apr 25 22:22:58 2006 +0200
+++ b/src/Pure/library.ML	Tue Apr 25 22:23:04 2006 +0200
@@ -115,6 +115,7 @@
   val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
   val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
+  val flat: 'a list list -> 'a list
   val unflat: 'a list list -> 'b list -> 'b list list
   val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
   val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
@@ -287,7 +288,6 @@
   val take: int * 'a list -> 'a list
   val drop: int * 'a list -> 'a list
   val last_elem: 'a list -> 'a
-  val flat: 'a list list -> 'a list
   val seq: ('a -> unit) -> 'a list -> unit
   val partition: ('a -> bool) -> 'a list -> 'a list * 'a list
   val mapfilter: ('a -> 'b option) -> 'a list -> 'b list
@@ -654,17 +654,16 @@
 fun get_index f =
   let
     fun get _ [] = NONE
-      | get i (x::xs) = 
+      | get i (x :: xs) =
           case f x
-           of NONE => get (i+1) xs
+           of NONE => get (i + 1) xs
             | SOME y => SOME (i, y)
   in get 0 end;
 
 fun eq_list _ ([], []) = true
-  | eq_list eq (x::xs, y::ys) = eq (x, y) andalso eq_list eq (xs, ys)
+  | eq_list eq (x :: xs, y :: ys) = eq (x, y) andalso eq_list eq (xs, ys)
   | eq_list _ _ = false;
 
-(*flatten a list of lists to a list*)
 val flat = List.concat;
 
 fun unflat (xs :: xss) ys =