src/HOL/Matrix/fspmlp.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
--- a/src/HOL/Matrix/fspmlp.ML	Thu Mar 03 09:22:35 2005 +0100
+++ b/src/HOL/Matrix/fspmlp.ML	Thu Mar 03 12:43:01 2005 +0100
@@ -145,7 +145,7 @@
 				     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 
@@ -234,7 +234,7 @@
 						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
@@ -251,7 +251,7 @@
 			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