diff -r 3633f560f4c3 -r 479806475f3c src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Sun Mar 01 16:48:06 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML	Sun Mar 01 23:36:12 2009 +0100
@@ -115,7 +115,7 @@
           then HOLogic.zero
           else foldl1 plus (ts @ [HOLogic.Suc_zero])
       in
-        foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
+        List.foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
       end;
 
     val fs = maps (fn (_, (name, _, constrs)) =>