# HG changeset patch
# User wenzelm
# Date 1146083891 -7200
# Node ID 70223ad978430f5522badcc3ad5fa8e5d85a4834
# Parent  d87a8838afa4117372f1b12f286f44b3536bc892
removed splitAt (superceded by chop);
removed if_none (superceded by the_default);

diff -r d87a8838afa4 -r 70223ad97843 src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Apr 26 22:38:05 2006 +0200
+++ b/src/Pure/library.ML	Wed Apr 26 22:38:11 2006 +0200
@@ -48,7 +48,6 @@
   val these: 'a list option -> 'a list
   val the_default: 'a -> 'a option -> 'a
   val the_list: 'a option -> 'a list
-  val if_none: 'a option -> 'a -> 'a
   val is_some: 'a option -> bool
   val is_none: 'a option -> bool
   val perhaps: ('a -> 'a option) -> 'a -> 'a
@@ -116,11 +115,11 @@
   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 maps: ('a -> 'b list) -> 'a list -> 'b 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
   val chop: int -> 'a list -> 'a list * 'a list
-  val splitAt: int * 'a list -> 'a list * 'a list
   val dropwhile: ('a -> bool) -> 'a list -> 'a list
   val nth: 'a list -> int -> 'a
   val nth_update: int * 'a -> 'a list -> 'a list
@@ -352,10 +351,6 @@
 fun the_list (SOME x) = [x]
   | the_list _ = []
 
-(*strict!*)
-fun if_none NONE y = y
-  | if_none (SOME x) _ = x;
-
 fun is_some (SOME _) = true
   | is_some NONE = false;
 
@@ -372,6 +367,7 @@
   | merge_opt _ (x, NONE) = x
   | merge_opt eq (SOME x, SOME y) = if eq (x, y) then SOME y else raise Option;
 
+
 (* exceptions *)
 
 val do_transform_failure = ref true;
@@ -587,8 +583,6 @@
   | chop _ [] = ([], [])
   | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
 
-fun splitAt (n, xs) = chop n xs;
-
 (*take the first n elements from a list*)
 fun take (n, []) = []
   | take (n, x :: xs) =
@@ -610,9 +604,9 @@
 
 (*update nth element*)
 fun nth_update (n, x) xs =
-    (case splitAt (n, xs) of
-      (_, []) => raise Subscript
-    | (prfx, _ :: sffx') => prfx @ (x :: sffx'))
+  (case chop n xs of
+    (_, []) => raise Subscript
+  | (prfx, _ :: sffx') => prfx @ (x :: sffx'));
 
 fun nth_map 0 f (x :: xs) = f x :: xs
   | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
@@ -666,6 +660,8 @@
 
 val flat = List.concat;
 
+fun maps f = flat o map f;
+
 fun unflat (xs :: xss) ys =
       let val (ps, qs) = chop (length xs) ys
       in ps :: unflat xss qs end
@@ -1095,7 +1091,7 @@
 fun fold_bal f [x] = x
   | fold_bal f [] = raise Balance
   | fold_bal f xs =
-      let val (ps,qs) = splitAt(length xs div 2, xs)
+      let val (ps, qs) = chop (length xs div 2) xs
       in  f (fold_bal f ps, fold_bal f qs)  end;
 
 (*construct something of the form f(...g(...(x)...)) for balanced access*)