src/HOL/Tools/Function/size.ML

--- a/src/HOL/Tools/Function/size.ML	Thu Oct 29 23:49:55 2009 +0100
+++ b/src/HOL/Tools/Function/size.ML	Thu Oct 29 23:56:33 2009 +0100
@@ -115,7 +115,7 @@
           then HOLogic.zero
           else foldl1 plus (ts @ [HOLogic.Suc_zero])
       in
-        List.foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
+        fold_rev (fn T => fn t' => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT) t
       end;
 
     val fs = maps (fn (_, (name, _, constrs)) =>