--- 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);