# HG changeset patch
# User haftmann
# Date 1276867562 -7200
# Node ID 802619d7576d51b0d68166681ec6372e7e057d47
# Parent  3489cea0e0e927023e65359b085065b92aa28d97
prefer fold over foldl

diff -r 3489cea0e0e9 -r 802619d7576d src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Fri Jun 18 15:03:21 2010 +0200
+++ b/src/HOL/Library/RBT.thy	Fri Jun 18 15:26:02 2010 +0200
@@ -143,7 +143,7 @@
   by (simp add: map_def lookup_RBT lookup_map lookup_impl_of)
 
 lemma fold_fold:
-  "fold f t = (\<lambda>s. foldl (\<lambda>s (k, v). f k v s) s (entries t))"
+  "fold f t = More_List.fold (prod_case f) (entries t)"
   by (simp add: fold_def expand_fun_eq RBT_Impl.fold_def entries_impl_of)
 
 lemma is_empty_empty [simp]: