src/Pure/library.ML
changeset 21118 d9789a87825d
parent 20972 db0425645cc7
child 21182 747ff99b35ee
     1.1 --- a/src/Pure/library.ML	Tue Oct 31 09:29:08 2006 +0100
     1.2 +++ b/src/Pure/library.ML	Tue Oct 31 09:29:11 2006 +0100
     1.3 @@ -46,7 +46,6 @@
     1.4    val is_some: 'a option -> bool
     1.5    val is_none: 'a option -> bool
     1.6    val perhaps: ('a -> 'a option) -> 'a -> 'a
     1.7 -  val merge_opt: ('a * 'a -> bool) -> 'a option * 'a option -> 'a option
     1.8  
     1.9    (*exceptions*)
    1.10    val try: ('a -> 'b) -> 'a -> 'b option
    1.11 @@ -119,7 +118,6 @@
    1.12    val chop: int -> 'a list -> 'a list * 'a list
    1.13    val dropwhile: ('a -> bool) -> 'a list -> 'a list
    1.14    val nth: 'a list -> int -> 'a
    1.15 -  val nth_update: int * 'a -> 'a list -> 'a list
    1.16    val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
    1.17    val nth_list: 'a list list -> int -> 'a list
    1.18    val map_index: (int * 'a -> 'b) -> 'a list -> 'b list
    1.19 @@ -350,10 +348,6 @@
    1.20  
    1.21  fun perhaps f x = the_default x (f x);
    1.22  
    1.23 -fun merge_opt _ (NONE, y) = y
    1.24 -  | merge_opt _ (x, NONE) = x
    1.25 -  | merge_opt eq (SOME x, SOME y) = if eq (x, y) then SOME y else raise Option;
    1.26 -
    1.27  
    1.28  (* exceptions *)
    1.29  
    1.30 @@ -549,12 +543,6 @@
    1.31              | itr (x::l) = f(x, itr l)
    1.32        in  itr l  end;
    1.33  
    1.34 -fun fold_index f =
    1.35 -  let
    1.36 -    fun fold_aux _ [] y = y
    1.37 -      | fold_aux i (x :: xs) y = fold_aux (i+1) xs (f (i, x) y);
    1.38 -  in fold_aux 0 end;
    1.39 -
    1.40  fun foldl_map f =
    1.41    let
    1.42      fun fold_aux (x, []) = (x, [])
    1.43 @@ -600,12 +588,6 @@
    1.44  
    1.45  fun nth_list xss i = nth xss i handle Subscript => [];
    1.46  
    1.47 -(*update nth element*)
    1.48 -fun nth_update (n, x) xs =
    1.49 -  (case chop n xs of
    1.50 -    (_, []) => raise Subscript
    1.51 -  | (prfx, _ :: sffx') => prfx @ (x :: sffx'));
    1.52 -
    1.53  fun nth_map 0 f (x :: xs) = f x :: xs
    1.54    | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
    1.55    | nth_map _ _ [] = raise Subscript;
    1.56 @@ -616,6 +598,12 @@
    1.57        | mapp i (x :: xs) = f (i, x) :: mapp (i+1) xs
    1.58    in mapp 0 end;
    1.59  
    1.60 +fun fold_index f =
    1.61 +  let
    1.62 +    fun fold_aux _ [] y = y
    1.63 +      | fold_aux i (x :: xs) y = fold_aux (i+1) xs (f (i, x) y);
    1.64 +  in fold_aux 0 end;
    1.65 +
    1.66  val last_elem = List.last;
    1.67  
    1.68  (*rear decomposition*)