made N2M tactic more robust
authortraytel
Thu Apr 10 09:38:38 2014 +0200 (2014-04-10)
changeset 56486753b779d070d
parent 56485 008634379465
child 56487 961b34963fa4
made N2M tactic more robust
src/HOL/Tools/BNF/bnf_fp_n2m.ML
     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