src/HOL/Tools/Nitpick/nitpick_hol.ML

            end
 
 fun ap_curry [_] _ t = t
   | ap_curry arg_Ts tuple_T t =
     let val n = length arg_Ts in
-      list_abs (map (pair "c") arg_Ts,
-                incr_boundvars n t
-                $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
+      fold_rev (Term.abs o pair "c") arg_Ts
+                (incr_boundvars n t $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
     end
 
 fun num_occs_of_bound_in_term j (t1 $ t2) =
     op + (pairself (num_occs_of_bound_in_term j) (t1, t2))
   | num_occs_of_bound_in_term j (Abs (_, _, t')) =

                            (disjuncts_of body)
           val base_body = nonrecs |> List.foldl s_disj @{const False}
           val step_body = recs |> map (repair_rec j)
                                |> List.foldl s_disj @{const False}
         in
-          (list_abs (tl xs, incr_bv (~1, j, base_body))
+          (fold_rev Term.abs (tl xs) (incr_bv (~1, j, base_body))
            |> ap_n_split (length arg_Ts) tuple_T bool_T,
-           Abs ("y", tuple_T, list_abs (tl xs, step_body)
+           Abs ("y", tuple_T, fold_rev Term.abs (tl xs) step_body
                               |> ap_n_split (length arg_Ts) tuple_T bool_T))
         end
       | aux t =
         raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
   in aux end

                 $ list_comb (Const step_x, outer_bounds))
     val image_set =
       image_const $ (rtrancl_const $ step_set) $ base_set
       |> predicatify tuple_T
   in
-    list_abs (outer, image_set |> ap_curry tuple_arg_Ts tuple_T)
+    fold_rev Term.abs outer (image_set |> ap_curry tuple_arg_Ts tuple_T)
     |> unfold_defs_in_term hol_ctxt
   end
 
 fun is_good_starred_linear_pred_type (Type (@{type_name fun}, Ts)) =
     forall (not o (is_fun_or_set_type orf is_pair_type)) Ts