src/HOL/Tools/Function/size.ML
changeset 33339 d41f77196338
parent 33056 791a4655cae3
child 33522 737589bb9bb8
     1.1 --- a/src/HOL/Tools/Function/size.ML	Thu Oct 29 23:49:55 2009 +0100
     1.2 +++ b/src/HOL/Tools/Function/size.ML	Thu Oct 29 23:56:33 2009 +0100
     1.3 @@ -115,7 +115,7 @@
     1.4            then HOLogic.zero
     1.5            else foldl1 plus (ts @ [HOLogic.Suc_zero])
     1.6        in
     1.7 -        List.foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
     1.8 +        fold_rev (fn T => fn t' => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT) t
     1.9        end;
    1.10  
    1.11      val fs = maps (fn (_, (name, _, constrs)) =>