--- 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));