# HG changeset patch
# User wenzelm
# Date 1266256216 -3600
# Node ID 7e24282f2dd7620ee299c86fd11438df999522ea
# Parent  0991c84e8dcf938086ac0cc34a46273272bc3e61
eliminated old fold;

diff -r 0991c84e8dcf -r 7e24282f2dd7 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon Feb 15 18:03:42 2010 +0100
+++ b/src/HOL/Tools/record.ML	Mon Feb 15 18:50:16 2010 +0100
@@ -674,7 +674,7 @@
 
 
 fun record_update_tr [t, u] =
-      Library.foldr (op $) (rev (gen_fields_tr "_updates" "_update" updateN u), t)
+      fold (curry op $) (gen_fields_tr "_updates" "_update" updateN u) t
   | record_update_tr ts = raise TERM ("record_update_tr", ts);
 
 fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts