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