prefer eta-expanded code equations for fold, to accomodate tail recursion optimisation in Scala

--- a/src/HOL/List.thy	Wed Aug 15 23:06:17 2012 +0200
+++ b/src/HOL/List.thy	Thu Aug 16 14:07:32 2012 +0200
@@ -2392,6 +2392,11 @@
 
 subsubsection {* @{const fold} with natural argument order *}
 
+lemma fold_simps [code]: -- {* eta-expanded variant for generated code -- enables tail-recursion optimisation in Scala *}
+  "fold f [] s = s"
+  "fold f (x # xs) s = fold f xs (f x s)" 
+  by simp_all
+
 lemma fold_remove1_split:
   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"
     and x: "x \<in> set xs"