abandoned foldl
authorhaftmann
Fri, 20 Oct 2006 10:44:51 +0200
changeset 21065 42669b5bf98e
parent 21064 9684dd7c81b5
child 21066 ce6759d1d0b4
abandoned foldl
src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Fri Oct 20 10:44:47 2006 +0200
+++ b/src/Pure/General/table.ML	Fri Oct 20 10:44:51 2006 +0200
@@ -26,7 +26,6 @@
   val map': (key -> 'a -> 'b) -> 'a table -> 'b table
   val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
   val fold_map: (key * 'b -> 'a -> 'c * 'a) -> 'b table -> 'a -> 'c table * 'a
-  val foldl: ('a * (key * 'b) -> 'a) -> 'a * 'b table -> 'a
   val dest: 'a table -> (key * 'a) list
   val keys: 'a table -> key list
   val min_key: 'a table -> key option
@@ -393,7 +392,6 @@
 fun map f = map_table (K f);
 val map' = map_table;
 val fold = fold_table;
-fun foldl f (x, tab) = fold (fn p => fn x' => f (x', p)) tab x;
 val fold_map = fold_map_table;
 
 end;