Removal of now unused sum, max, min. Use foldl op+, Int.max, Int.min
authorpaulson
Mon, 04 Nov 1996 10:54:26 +0100
changeset 2157 50c26585e523
parent 2156 9c361df93bd5
child 2158 77dfe65b5bb3
Removal of now unused sum, max, min. Use foldl op+, Int.max, Int.min
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;