dropped nth_update

--- a/NEWS	Mon Oct 30 16:42:46 2006 +0100
+++ b/NEWS	Tue Oct 31 09:28:52 2006 +0100
@@ -693,7 +693,6 @@
 functions for alists, tables, etc:
 
   val nth: 'a list -> int -> 'a 
-  val nth_update: int * 'a -> 'a list -> 'a list
   val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
   val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
 
@@ -703,7 +702,7 @@
 * Pure/library: general ``divide_and_conquer'' combinator on lists.
 
 * Pure/General/name_mangler.ML provides a functor for generic name
-mangling (bijective mapping from any expression values to strings).
+mangling (bijective mapping from expression values to strings).
 
 * Pure/General/rat.ML implements rational numbers.
 

--- a/src/HOL/Tools/record_package.ML	Mon Oct 30 16:42:46 2006 +0100
+++ b/src/HOL/Tools/record_package.ML	Tue Oct 31 09:28:52 2006 +0100
@@ -1410,7 +1410,7 @@
     (*updates*)
     fun mk_upd_prop (i,(c,T)) =
       let val x' = Free (Name.variant variants (base c ^ "'"),T)
-          val args' = nth_update (i, x') vars_more
+          val args' = nth_map i (K x') vars_more
       in mk_upd updN c x' ext === mk_ext args'  end;
     val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
 
@@ -1788,7 +1788,7 @@
     (*updates*)
     fun mk_upd_prop (i,(c,T)) =
       let val x' = Free (Name.variant all_variants (base c ^ "'"),T)
-          val args' = nth_update (parent_fields_len + i, x') all_vars_more
+          val args' = nth_map (parent_fields_len + i) (K x') all_vars_more
       in mk_upd updateN c x' r_rec0 === mk_rec args' 0  end;
     val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
 

--- a/src/Provers/Arith/fast_lin_arith.ML	Mon Oct 30 16:42:46 2006 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Oct 31 09:28:52 2006 +0100
@@ -223,18 +223,18 @@
                     in if Rat.le (lb, ub') then ub' else raise NoEx end;
 
 fun findex1 discr (ex, (v, lineqs)) =
-  let val nz = List.filter (fn (Lineq(_,_,cs,_)) => el v cs <> 0) lineqs;
+  let val nz = filter (fn (Lineq (_, _, cs, _)) => el v cs <> 0) lineqs;
       val ineqs = Library.foldl elim_eqns ([],nz)
       val (ge,le) = List.partition (fn (_,_,cs) => el v cs > 0) ineqs
       val lb = ratrelmax (map (eval ex v) ge)
       val ub = ratrelmin (map (eval ex v) le)
-  in nth_update (v, choose2 (nth discr v) (lb, ub)) ex end;
+  in nth_map v (K (choose2 (nth discr v) (lb, ub))) ex end;
 
 fun findex discr = Library.foldl (findex1 discr);
 
 fun elim1 v x =
   map (fn (a,le,bs) => (Rat.add (a, Rat.neg (Rat.mult (el v bs, x))), le,
-                        nth_update (v, Rat.zero) bs));
+                        nth_map v (K Rat.zero) bs));
 
 fun single_var v (_,_,cs) = (filter_out (equal Rat.zero) cs = [el v cs]);
 
@@ -256,7 +256,7 @@
            val bnds = map (fn (a,le,bs) => (Rat.mult(a,Rat.inv(el v bs)),le)) sv
            val x = minmax((Rat.zero,if pos then true else false)::bnds)
            val ineqs' = elim1 v x nz
-           val ex' = nth_update (v, x) ex
+           val ex' = nth_map v (K x) ex
        in pick_vars discr (ineqs',ex') end
   end;