src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 56486 753b779d070d
parent 56484 c451cf8b29c8
child 56487 961b34963fa4
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Apr 09 18:40:21 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Apr 10 09:38:38 2014 +0200
     1.3 @@ -373,7 +373,8 @@
     1.4  
     1.5      val co_recs = map (Morphism.term phi) raw_co_recs;
     1.6  
     1.7 -    val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_map_thms;
     1.8 +    val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_map_thms
     1.9 +      |> maps (fn thm => [thm, thm RS rewrite_comp_comp]);
    1.10  
    1.11      val xtor_co_rec_thms =
    1.12        let