src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML

   let
     val thy = Proof_Context.theory_of ctxt;
 
     fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else ();
 
-    fun massage_rec bound_Ts t =
+    fun massage_abs bound_Ts (Abs (s, T, t)) = massage_abs (T :: bound_Ts) t
+      | massage_abs bound_Ts t = massage_rec bound_Ts t
+    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}, _), [arg1, arg2]) =>
           massage_rec bound_Ts (betapply (arg2, arg1))
-        | (Const (@{const_name If}, _), obj :: (branches as [then_branch, _])) =>
+        | (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
         | (Const (c, _), args as _ :: _) =>
           let val n = num_binder_types (Sign.the_const_type thy c) in

               (case fastype_of1 (bound_Ts, nth args (n - 1)) of
                 Type (s, Ts) =>
                 if case_of ctxt s = SOME c then
                   let
                     val (branches, obj_leftovers) = chop n args;
-                    val branches' = map (massage_rec bound_Ts) branches;
+                    val branches' = map (massage_abs bound_Ts o Envir.eta_long bound_Ts) branches;
                     val casex' = Const (c, map typof branches' ---> map typof obj_leftovers --->
                       typof t);
                   in
                     betapplys (casex', branches' @ tap (List.app check_no_call) obj_leftovers)
                   end

   | NONE => raise Fail "expand_ctr_term");
 
 fun expand_corec_code_rhs ctxt has_call bound_Ts t =
   (case fastype_of1 (bound_Ts, t) of
     Type (s, Ts) =>
-    massage_let_if_case ctxt has_call (fn bound_Ts => fn t =>
+    massage_let_if_case ctxt has_call (fn _ => fn t =>
       if can (dest_ctr ctxt s) t then t else expand_ctr_term ctxt s Ts t) bound_Ts t
   | _ => raise Fail "expand_corec_code_rhs");
 
 fun massage_corec_code_rhs ctxt massage_ctr =
   massage_let_if_case ctxt (K false)