equal
deleted
inserted
replaced
281 hd x |> #left_args |> length) funs_data; |
281 hd x |> #left_args |> length) funs_data; |
282 in |
282 in |
283 (recs, ctr_poss) |
283 (recs, ctr_poss) |
284 |-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos) |
284 |-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos) |
285 |> Syntax.check_terms lthy |
285 |> Syntax.check_terms lthy |
286 |> map3 (fn b => fn mx => fn t => |
286 |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t))) |
287 ((b, mx), ((Binding.conceal (Binding.map_name Thm.def_name b), []), t))) bs mxs |
287 bs mxs |
288 end; |
288 end; |
289 |
289 |
290 fun find_rec_calls has_call (eqn_data : eqn_data) = |
290 fun find_rec_calls has_call (eqn_data : eqn_data) = |
291 let |
291 let |
292 fun find (Abs (_, _, b)) ctr_arg = find b ctr_arg |
292 fun find (Abs (_, _, b)) ctr_arg = find b ctr_arg |
776 in |
776 in |
777 map (list_comb o rpair corec_args) corecs |
777 map (list_comb o rpair corec_args) corecs |
778 |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss |
778 |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss |
779 |> map2 currys arg_Tss |
779 |> map2 currys arg_Tss |
780 |> Syntax.check_terms lthy |
780 |> Syntax.check_terms lthy |
781 |> map3 (fn b => fn mx => fn t => |
781 |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t))) |
782 ((b, mx), ((Binding.conceal (Binding.map_name Thm.def_name b), []), t))) bs mxs |
782 bs mxs |
783 |> rpair exclss' |
783 |> rpair exclss' |
784 end; |
784 end; |
785 |
785 |
786 fun mk_real_disc_eqns fun_binding arg_Ts ({ctr_specs, ...} : corec_spec) |
786 fun mk_real_disc_eqns fun_binding arg_Ts ({ctr_specs, ...} : corec_spec) |
787 (sel_eqns : coeqn_data_sel list) (disc_eqns : coeqn_data_disc list) = |
787 (sel_eqns : coeqn_data_sel list) (disc_eqns : coeqn_data_disc list) = |