Removal of now unused sum, max, min. Use foldl op+, Int.max, Int.min
authorpaulson
Mon Nov 04 10:54:26 1996 +0100 (1996-11-04)
changeset 215750c26585e523
parent 2156 9c361df93bd5
child 2158 77dfe65b5bb3
Removal of now unused sum, max, min. Use foldl op+, Int.max, Int.min
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Fri Nov 01 18:34:34 1996 +0100
     1.2 +++ b/src/Pure/library.ML	Mon Nov 04 10:54:26 1996 +0100
     1.3 @@ -330,20 +330,6 @@
     1.4    | downto0 ([], n) = n = ~1;
     1.5  
     1.6  
     1.7 -(* operations on integer lists *)
     1.8 -
     1.9 -fun sum [] = 0
    1.10 -  | sum (n :: ns) = n + sum ns;
    1.11 -
    1.12 -fun max [m:int] = m
    1.13 -  | max (m :: n :: ns) = if m > n then max (m :: ns) else max (n :: ns)
    1.14 -  | max [] = raise LIST "max";
    1.15 -
    1.16 -fun min [m:int] = m
    1.17 -  | min (m :: n :: ns) = if m < n then min (m :: ns) else min (n :: ns)
    1.18 -  | min [] = raise LIST "min";
    1.19 -
    1.20 -
    1.21  (* convert integers to strings *)
    1.22  
    1.23  (*expand the number in the given base;