# HG changeset patch
# User paulson
# Date 846859269 -3600
# Node ID 084218afaf4b8266ac8dc640181ea7d421bfebdc
# Parent  639db817780404e767f478ef414a546591784877
Replaced "sum" (only usage?) by foldl op+

diff -r 639db8177804 -r 084218afaf4b src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Fri Nov 01 15:39:37 1996 +0100
+++ b/src/Pure/Thy/thm_database.ML	Fri Nov 01 15:41:09 1996 +0100
@@ -202,7 +202,9 @@
       fun substsize(prop, tsig) =
             let val Some pat = extract prop
                 val (_,subst) = Pattern.match tsig (pat,obj)
-            in sum(map (fn (_,t) => size_of_term t) subst) end
+            in foldl op+
+		(0, map (fn (_,t) => size_of_term t) subst)
+            end
 
       fun thm_order ((p0:int,s0:int,_),(p1,s1,_)) =
             (((p0=0 andalso p1=0) orelse (p0<>0 andalso p1<>0)) andalso s0<=s1)