Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/function_package/size.ML
changeset 30190 479806475f3c
parent 29866 6e93ae65c678
child 30280 eb98b49ef835 
--- 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)) =>
isabelle