equal
deleted
inserted
replaced
883 let |
883 let |
884 val corecs = map #corec corec_specs; |
884 val corecs = map #corec corec_specs; |
885 val ctr_specss = map #ctr_specs corec_specs; |
885 val ctr_specss = map #ctr_specs corec_specs; |
886 val corec_args = hd corecs |
886 val corec_args = hd corecs |
887 |> fst o split_last o binder_types o fastype_of |
887 |> fst o split_last o binder_types o fastype_of |
888 |> map (fn T => if range_type T = HOLogic.boolT |
888 |> map (fn T => |
889 then Abs (Name.uu_, domain_type T, @{term False}) |
889 if range_type T = HOLogic.boolT then Abs (Name.uu_, domain_type T, @{term False}) |
890 else Const (@{const_name undefined}, T)) |
890 else Const (@{const_name undefined}, T)) |
891 |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss |
891 |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss |
892 |> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss; |
892 |> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss; |
893 |
893 |
894 fun currys [] t = t |
894 fun currys [] t = t |