src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
changeset 53678 e55bb583342e
parent 53591 b6e2993fd0d3
child 53746 bd038e48526d
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Sep 17 00:48:01 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Sep 17 01:09:51 2013 +0200
     1.3 @@ -158,8 +158,8 @@
     1.4            derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
     1.5              dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
     1.6              ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
     1.7 -          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _, _,
     1.8 -                  (disc_unfold_thmss, disc_corec_thmss, _),
     1.9 +          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _,
    1.10 +                  (disc_unfold_thmss, disc_corec_thmss, _), _,
    1.11                    (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
    1.12              (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
    1.13               disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss));