src/HOL/Tools/Function/size.ML

         val t =
           if null ts andalso (not b orelse not (exists (is_poly thy) cargs'))
           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)) =>
       map (size_of_constr true param_size) (constrs ~~ constrs_of thy name)) descr;
     val fs' = maps (fn (n, (name, _, constrs)) =>