# HG changeset patch
# User blanchet
# Date 1379372991 -7200
# Node ID e55bb583342e37f2d46f9ea8dbd81f671357d1a4
# Parent  b51ebeda414d00a3c7b3f085252dc8be33b0023a
return right theorems

diff -r b51ebeda414d -r e55bb583342e src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Sep 17 00:48:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Sep 17 01:09:51 2013 +0200
@@ -158,8 +158,8 @@
           derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
             dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
             ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
-          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _, _,
-                  (disc_unfold_thmss, disc_corec_thmss, _),
+          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _,
+                  (disc_unfold_thmss, disc_corec_thmss, _), _,
                   (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
             (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
              disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss));