src/HOL/Matrix/fspmlp.ML

 			      | SOME x => 
 				(case get_sure_bound g src_key of
 				     NONE => NONE
 				   | SOME src_sure_bound => SOME (FloatArith.add x (mult_btype src_sure_bound coeff)))
 		    in
-			case foldl add_src_bound (SOME row_bound, sources) of
+			case Library.foldl add_src_bound (SOME row_bound, sources) of
 			    NONE => sure_bound
 			  | new_sure_bound as (SOME new_bound) => 
 			    (case sure_bound of 
 				 NONE => new_sure_bound
 			       | SOME old_bound => 

 						add_edge g (src_index, UPPER) dest_key row_index coeff
 					    else
 						add_edge g (src_index, LOWER) dest_key row_index coeff
 					end
 			    in	    
-				foldl fold_src_nodes ((add_row_bound g dest_key row_index row_bound), approx_a)
+				Library.foldl fold_src_nodes ((add_row_bound g dest_key row_index row_bound), approx_a)
 			    end
 		    end
 	    in
 		case approx_a of
 		    [] => g

 			else if atest = 1 then
 			    update_sure_bound g (u, UPPER) b2
 			else
 			    g
 		    end
-		  | _ => foldl fold_dest_nodes (g, approx_a)
+		  | _ => Library.foldl fold_dest_nodes (g, approx_a)
 	    end
 	
 	val g = FloatSparseMatrixBuilder.m_fold calcr VarGraph.empty A
 	val g = propagate_sure_bounds safe_propagation names g