src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML

     val bad = fold (add_extra_frees ctxt [] []) corec_args [];
     val _ = null bad orelse
       (if exists has_call corec_args then nonprimitive_corec ctxt []
        else extra_variable ctxt [] (hd bad));
 
-    fun currys [] t = t
-      | currys Ts t = t $ mk_tuple1_balanced (List.rev Ts) (map Bound (length Ts - 1 downto 0))
-          |> fold_rev (Term.abs o pair Name.uu) Ts;
-
     val excludess' =
       disc_eqnss
       |> map (map (fn x => (#fun_args x, #ctr_no x, #prems x, #auto_gen x))
         #> fst o (fn xs => fold_map (fn x => fn ys => ((x, ys), ys @ [x])) xs [])
         #> maps (uncurry (map o pair)

             ||> map_prod (map HOLogic.mk_Trueprop) HOLogic.mk_Trueprop
             ||> Logic.list_implies
             ||> curry Logic.list_all (map dest_Free fun_args))));
   in
     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
+    |> map2 abs_curried_balanced arg_Tss
     |> (fn ts => Syntax.check_terms ctxt ts
       handle ERROR _ => nonprimitive_corec ctxt [])
     |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t)))
       bs mxs
     |> rpair excludess'