# HG changeset patch
# User paulson
# Date 847101266 -3600
# Node ID 50c26585e5231f7c8aeebd67434bbc70a7e24239
# Parent  9c361df93bd5874bf4e27f6e3eec71cca44d3fee
Removal of now unused sum, max, min.  Use foldl op+, Int.max, Int.min

diff -r 9c361df93bd5 -r 50c26585e523 src/Pure/library.ML
--- 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;