# HG changeset patch
# User blanchet
# Date 1427908661 -7200
# Node ID 2d929c17828389227d611496fb4683fcff2d6ce6
# Parent  db4000b71fdbf445c51fd6b91b6dddca666ba4ef
simplified code

diff -r db4000b71fdb -r 2d929c178283 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Apr 01 16:04:21 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Apr 01 19:17:41 2015 +0200
@@ -155,6 +155,7 @@
   val Inr_const: typ -> typ -> term
   val mk_tuple_balanced: term list -> term
   val mk_tuple1_balanced: typ list -> term list -> term
+  val abs_curried_balanced: typ list -> term -> term
 
   val mk_case_sum: term * term -> term
   val mk_case_sumN: term list -> term
@@ -437,6 +438,10 @@
 
 val mk_tuple_balanced = mk_tuple1_balanced [];
 
+fun abs_curried_balanced 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;
+
 fun mk_sumprod_balanced T n k ts = Sum_Tree.mk_inj T n k (mk_tuple_balanced ts);
 
 fun mk_absumprod absT abs0 n k ts =
diff -r db4000b71fdb -r 2d929c178283 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Apr 01 16:04:21 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Apr 01 19:17:41 2015 +0200
@@ -964,10 +964,6 @@
       (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))
@@ -980,8 +976,7 @@
             ||> 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)))