src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 57303 498a62e65f5f
parent 56650 1f9ab71d43a5
child 57397 5004aca20821
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Jun 24 13:48:14 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Jun 24 13:48:14 2014 +0200
     1.3 @@ -340,11 +340,11 @@
     1.4                        val (TY, (U, X)) = TU |> dest_co_algT ||> dest_co_productT;
     1.5                        val T = mk_co_algT TY U;
     1.6                      in
     1.7 -                      (case try (force_typ names_lthy T o build_map lthy co_proj1_const o dest_funT) T of
     1.8 +                      (case try (force_typ names_lthy T o build_map lthy [] co_proj1_const o dest_funT) T of
     1.9                          SOME f => mk_co_product f
    1.10                            (fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X))))
    1.11                        | NONE => mk_map_co_product
    1.12 -                          (build_map lthy co_proj1_const
    1.13 +                          (build_map lthy [] co_proj1_const
    1.14                              (dest_funT (mk_co_algT (dest_co_productT TY |> fst) U)))
    1.15                            (HOLogic.id_const X))
    1.16                      end)