src/HOL/Matrix/cplex/CplexMatrixConverter.ML

           | setprod vec positive (cplexVar v) = set_elem vec (s2i v) (if positive then "1" else "-1")
           | setprod vec positive (cplexProd (cplexNum num, cplexVar v)) = 
             set_elem vec (s2i v) (if positive then num else "-"^num)
           | setprod _ _ _ = raise (Converter "term is not a normed product")        
 
-        fun sum2vec (cplexSum ts) = Library.foldl (fn (vec, t) => setprod vec true t) (empty_vector, ts)
+        fun sum2vec (cplexSum ts) = fold (fn t => fn vec => setprod vec true t) ts empty_vector
           | sum2vec t = setprod empty_vector true t                                                
 
         fun constrs2Ab j A b [] = (A, b)
           | constrs2Ab j A b ((_, cplexConstr (cplexLeq, (t1,t2)))::cs) = 
             constrs2Ab (j+1) (set_vector A j (sum2vec t1)) (set_elem b j (num2str true t2)) cs

         (goal_maximize, sum2vec goal_term, A, b, (varcount, i2s, s2i))
     end
 
 fun convert_results (cplex.Optimal (opt, entries)) name2index =
     let
-        fun setv (v, (name, value)) = (matrix_builder.set_elem v (name2index name) value) 
+        fun setv (name, value) v = matrix_builder.set_elem v (name2index name) value
     in
-        (opt, Library.foldl setv (matrix_builder.empty_vector, entries))
+        (opt, fold setv entries (matrix_builder.empty_vector))
     end
   | convert_results _ _ = raise (Converter "No optimal result")
 
 end;