src/HOL/Codatatype/Tools/bnf_gfp.ML
changeset 49255 2ecc533d6697
parent 49231 43d2df313559
child 49277 aee77001243f
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Mon Sep 10 17:32:39 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Mon Sep 10 17:35:53 2012 +0200
     1.3 @@ -506,7 +506,7 @@
     1.4      val mor_sum_case_thm =
     1.5        let
     1.6          val maps = map3 (fn s => fn sum_s => fn map =>
     1.7 -          mk_sum_case (HOLogic.mk_comp (Term.list_comb (map, passive_ids @ Inls), s)) sum_s)
     1.8 +          mk_sum_case (HOLogic.mk_comp (Term.list_comb (map, passive_ids @ Inls), s), sum_s))
     1.9            s's sum_ss map_Inls;
    1.10        in
    1.11          Skip_Proof.prove lthy [] []
    1.12 @@ -2144,7 +2144,7 @@
    1.13        let
    1.14          val corecT = Library.foldr (op -->) (corec_sTs, AT --> T);
    1.15          val maps = map3 (fn unf => fn sum_s => fn map => mk_sum_case
    1.16 -            (HOLogic.mk_comp (Term.list_comb (map, passive_ids @ corec_Inls), unf)) sum_s)
    1.17 +            (HOLogic.mk_comp (Term.list_comb (map, passive_ids @ corec_Inls), unf), sum_s))
    1.18            unfs corec_ss corec_maps;
    1.19  
    1.20          val lhs = Term.list_comb (Free (corec_name i, corecT), corec_ss);
    1.21 @@ -2171,7 +2171,7 @@
    1.22      val corec_defs = map (Morphism.thm phi) corec_def_frees;
    1.23  
    1.24      val sum_cases =
    1.25 -      map2 (fn T => fn i => mk_sum_case (HOLogic.id_const T) (mk_corec corec_ss i)) Ts ks;
    1.26 +      map2 (fn T => fn i => mk_sum_case (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks;
    1.27      val corec_thms =
    1.28        let
    1.29          fun mk_goal i corec_s corec_map unf z =