src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML

   let
     val thy = Proof_Context.theory_of ctxt;
 
     fun fld conds t =
       (case Term.strip_comb t of
-        (Const (@{const_name Let}, _), [_, _]) => fld conds (unfold_let t)
+        (Const (@{const_name Let}, _), [_, _]) => fld conds (unfold_lets_splits t)
       | (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
         fld (conds @ conjuncts_s cond) then_branch o fld (conds @ s_not_conj [cond]) else_branch
       | (Const (c, _), args as _ :: _ :: _) =>
         let val n = num_binder_types (Sign.the_const_type thy c) - 1 in
           if n >= 0 andalso n < length args then

           Abs (Name.uu, T, massage_abs (T :: bound_Ts) (m - 1) (incr_boundvars 1 t $ Bound 0))
         end
     and massage_rec bound_Ts t =
       let val typof = curry fastype_of1 bound_Ts in
         (case Term.strip_comb t of
-          (Const (@{const_name Let}, _), [_, _]) => massage_rec bound_Ts (unfold_let t)
+          (Const (@{const_name Let}, _), [_, _]) => massage_rec bound_Ts (unfold_lets_splits t)
         | (Const (@{const_name If}, _), obj :: (branches as [_, _])) =>
           let val branches' = map (massage_rec bound_Ts) branches in
             Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches')
           end
+        | (c as Const (@{const_name prod_case}, _), arg :: args) =>
+          massage_rec bound_Ts
+            (unfold_lets_splits (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
         | (Const (c, _), args as _ :: _ :: _) =>
           (case try strip_fun_type (Sign.the_const_type thy c) of
             SOME (gen_branch_Ts, gen_body_fun_T) =>
             let
               val gen_branch_ms = map num_binder_types gen_branch_Ts;

     eqn_pos eqn0 code_rhs_opt prems concl matchedsss =
   let
     val (lhs, rhs) = HOLogic.dest_eq concl;
     val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free;
     val SOME basic_ctr_specs = AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name;
-    val (ctr, ctr_args) = strip_comb (unfold_let rhs);
+    val (ctr, ctr_args) = strip_comb (unfold_lets_splits rhs);
     val {disc, sels, ...} = the (find_first (curry (op =) ctr o #ctr) basic_ctr_specs)
       handle Option.Option => primcorec_error_eqn "not a constructor" ctr;
 
     val disc_concl = betapply (disc, lhs);
     val (eqn_data_disc_opt, matchedsss') =

     val ctr_premss = (case cond_ctrs of [_] => [[]] | _ => map (s_dnf o snd) cond_ctrs);
     val ctr_concls = cond_ctrs |> map (fn (ctr, _) =>
         binder_types (fastype_of ctr)
         |> map_index (fn (n, T) => massage_corec_code_rhs lthy (fn _ => fn ctr' => fn args =>
           if ctr' = ctr then nth args n else Const (@{const_name undefined}, T)) [] rhs')
-        |> curry list_comb ctr
+        |> curry Term.list_comb ctr
         |> curry HOLogic.mk_eq lhs);
 
     val sequentials = replicate (length fun_names) false;
   in
     fold_map2 (dissect_coeqn_ctr fun_names sequentials basic_ctr_specss eqn_pos eqn0

       |>> single
     else if member (op =) sels head then
       ([dissect_coeqn_sel fun_names basic_ctr_specss eqn_pos NONE NONE eqn0 of_spec_opt concl],
        matchedsss)
     else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) then
-      if member (op =) ctrs (head_of (unfold_let (the rhs_opt))) then
+      if member (op =) ctrs (head_of (unfold_lets_splits (the rhs_opt))) then
         dissect_coeqn_ctr fun_names sequentials basic_ctr_specss eqn_pos eqn0
           (if null prems then
              SOME (snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_assums_concl eqn0))))
            else
              NONE)

             | rewrite bound_Ts (t as _ $ _) =
               let val (u, vs) = strip_comb t in
                 if is_Free u andalso has_call u then
                   Inr_const U T $ mk_tuple1 bound_Ts vs
                 else if try (fst o dest_Const) u = SOME @{const_name prod_case} then
-                  map (rewrite bound_Ts) vs |> chop 1 |>> HOLogic.mk_split o the_single |> list_comb
+                  map (rewrite bound_Ts) vs |> chop 1
+                  |>> HOLogic.mk_split o the_single
+                  |> Term.list_comb
                 else
-                  list_comb (rewrite bound_Ts u, map (rewrite bound_Ts) vs)
+                  Term.list_comb (rewrite bound_Ts u, map (rewrite bound_Ts) vs)
               end
             | rewrite _ t =
               if is_Free t andalso has_call t then Inr_const U T $ HOLogic.unit else t;
           in
             rewrite bound_Ts

               ((c, c', a orelse a'), (x, s_not (s_conjs y)))
             ||> apfst (map HOLogic.mk_Trueprop) o apsnd HOLogic.mk_Trueprop
             ||> Logic.list_implies
             ||> curry Logic.list_all (map dest_Free fun_args))));
   in
-    map (list_comb o rpair corec_args) corecs
+    map (Term.list_comb o rpair corec_args) corecs
     |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss
     |> map2 currys arg_Tss
     |> Syntax.check_terms lthy
     |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
       bs mxs

     K (if has_call rhs_term then fold_rev_let_if_case ctxt (K cons) [] rhs_term [] else [])
     |> nth_map sel_no |> AList.map_entry (op =) ctr
   end;
 
 fun applied_fun_of fun_name fun_T fun_args =
-  list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
+  Term.list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
 
 fun is_trivial_implies thm =
   uncurry (member (op aconv)) (Logic.strip_horn (Thm.prop_of thm));
 
 fun add_primcorec_ursive auto opts fixes specs of_specs_opt lthy =

                   SOME rhs => rhs
                 | NONE =>
                   filter (curry (op =) ctr o #ctr) sel_eqns
                   |> fst o finds (op = o apsnd #sel) sels
                   |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) #-> abstract)
-                  |> curry list_comb ctr)
+                  |> curry Term.list_comb ctr)
                 |> curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
                 |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
                 |> curry Logic.list_all (map dest_Free fun_args);
               val disc_thm_opt = AList.lookup (op =) disc_alist disc;
               val sel_thms = map snd (filter (member (op =) sels o fst) sel_alist);

                             val t =
                               filter (curry (op =) ctr o #ctr) sel_eqns
                               |> fst o finds (op = o apsnd #sel) sels
                               |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x))
                                 #-> abstract)
-                              |> curry list_comb ctr;
+                              |> curry Term.list_comb ctr;
                           in
                             SOME (prems, t)
                           end;
                       val ctr_conds_argss_opt = map prove_code_ctr ctr_specs;
                       val exhaustive_code =