# HG changeset patch
# User traytel
# Date 1397115518 -7200
# Node ID 753b779d070dca6fc4f6fd8179d95143f7a7cfba
# Parent  00863437946594265b93ccd42ab0763aa20d0d40
made N2M tactic more robust

diff -r 008634379465 -r 753b779d070d src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Apr 09 18:40:21 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Apr 10 09:38:38 2014 +0200
@@ -373,7 +373,8 @@
 
     val co_recs = map (Morphism.term phi) raw_co_recs;
 
-    val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_map_thms;
+    val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_map_thms
+      |> maps (fn thm => [thm, thm RS rewrite_comp_comp]);
 
     val xtor_co_rec_thms =
       let