src/Pure/Syntax/syn_trans.ML

     if ! eta_contract then eta_abs tm else tm
   end;
 
 
 fun abs_tr' tm =
-  Library.foldr (fn (x, t) => Lexicon.const "_abs" $ x $ t)
+  uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t))
     (strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
 
 fun atomic_abs_tr' (x, T, t) =
   let val [xT] = rename_wrt_term t [(x, T)]
   in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end;