diff -r ecf6375e2abb -r 426ed18eba43 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/HOL/Tools/record.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -1484,8 +1484,8 @@
                 NONE => error "try_param_tac: no such variable"
               | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
           | (_, T) :: _ =>
-              [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
-                (x, list_abs (params, Bound 0))])) rule';
+              [(P, fold_rev Term.abs params (if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
+                (x, fold_rev Term.abs params (Bound 0))])) rule';
   in compose_tac (false, rule'', nprems_of rule) i end);