src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
changeset 56978 0c1b4987e6b2
parent 56956 7425fa3763ff
child 56991 8e9ca31e9b8e
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri May 16 09:19:15 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri May 16 12:56:39 2014 +0200
     1.3 @@ -1146,10 +1146,11 @@
     1.4                fun mk_map_thm ctr_def' cxIn =
     1.5                  fold_thms lthy [ctr_def']
     1.6                    (unfold_thms lthy (o_apply :: pre_map_def ::
     1.7 -                       (if fp = Least_FP then [] else [ctor_dtor, dtor_ctor]) @ sumprod_thms_map @
     1.8 +                       (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_map @
     1.9                         abs_inverses)
    1.10                       (cterm_instantiate_pos (nones @ [SOME cxIn])
    1.11 -                        (if fp = Least_FP then fp_map_thm else fp_map_thm RS ctor_cong)))
    1.12 +                        (if fp = Least_FP then fp_map_thm
    1.13 +                         else fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans))))
    1.14                  |> singleton (Proof_Context.export names_lthy no_defs_lthy);
    1.15  
    1.16                fun mk_set_thm fp_set_thm ctr_def' cxIn =