--- 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 =
--- 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)))