src/HOL/Matrix/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) = foldl (fn (vec, t) => setprod vec true t) (empty_vector, ts)
+	fun sum2vec (cplexSum ts) = Library.foldl (fn (vec, t) => setprod vec true t) (empty_vector, ts)
 	  | 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

 
 fun convert_results (cplex.Optimal (opt, entries)) name2index =
     let
 	fun setv (v, (name, value)) = (matrix_builder.set_elem v (name2index name) value) 
     in
-	(opt, foldl setv (matrix_builder.empty_vector, entries))
+	(opt, Library.foldl setv (matrix_builder.empty_vector, entries))
     end
   | convert_results _ _ = raise (Converter "No optimal result")
     
 
 end;