# HG changeset patch
# User wenzelm
# Date 1279629673 -7200
# Node ID 1ce77362598f10890a6887bb246e13d38f1f5c6b
# Parent  afb5653a3a471d6c19c7dd1930f82c7e9235cc7b
tuned;

diff -r afb5653a3a47 -r 1ce77362598f src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Jul 20 11:11:15 2010 +0200
+++ b/src/Pure/library.ML	Tue Jul 20 14:41:13 2010 +0200
@@ -1000,21 +1000,23 @@
 (*Partition a list into buckets  [ bi, b(i+1), ..., bj ]
    putting x in bk if p(k)(x) holds.  Preserve order of elements if possible.*)
 fun partition_list p i j =
-  let fun part k xs =
-            if k>j then
-              (case xs of [] => []
-                         | _ => raise Fail "partition_list")
-            else
-            let val (ns, rest) = List.partition (p k) xs;
-            in  ns :: part(k+1)rest  end
-  in  part (i: int) end;
+  let
+    fun part (k: int) xs =
+      if k > j then
+        (case xs of
+          [] => []
+        | _ => raise Fail "partition_list")
+      else
+        let val (ns, rest) = List.partition (p k) xs
+        in ns :: part (k + 1) rest end;
+  in part (i: int) end;
 
-fun partition_eq (eq:'a * 'a -> bool) =
+fun partition_eq (eq: 'a * 'a -> bool) =
   let
     fun part [] = []
       | part (x :: ys) =
           let val (xs, xs') = List.partition (fn y => eq (x, y)) ys
-          in (x::xs)::(part xs') end
+          in (x :: xs) :: part xs' end;
   in part end;