1.1 --- a/src/HOL/List.thy	Wed Aug 15 23:06:17 2012 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Aug 16 14:07:32 2012 +0200
     1.3 @@ -2392,6 +2392,11 @@
     1.4  
     1.5  subsubsection {* @{const fold} with natural argument order *}
     1.6  
     1.7 +lemma fold_simps [code]: -- {* eta-expanded variant for generated code -- enables tail-recursion optimisation in Scala *}
     1.8 +  "fold f [] s = s"
     1.9 +  "fold f (x # xs) s = fold f xs (f x s)" 
    1.10 +  by simp_all
    1.11 +
    1.12  lemma fold_remove1_split:
    1.13    assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
    1.14      and x: "x \<in> set xs"