Removal of now unused sum, max, min. Use foldl op+, Int.max, Int.min
--- a/src/Pure/library.ML Fri Nov 01 18:34:34 1996 +0100
+++ b/src/Pure/library.ML Mon Nov 04 10:54:26 1996 +0100
@@ -330,20 +330,6 @@
| downto0 ([], n) = n = ~1;
-(* operations on integer lists *)
-
-fun sum [] = 0
- | sum (n :: ns) = n + sum ns;
-
-fun max [m:int] = m
- | max (m :: n :: ns) = if m > n then max (m :: ns) else max (n :: ns)
- | max [] = raise LIST "max";
-
-fun min [m:int] = m
- | min (m :: n :: ns) = if m < n then min (m :: ns) else min (n :: ns)
- | min [] = raise LIST "min";
-
-
(* convert integers to strings *)
(*expand the number in the given base;