src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
changeset 54235 3aed2ae6eb91
parent 54234 b5310a1b807c
child 54239 9bd91d5d8a7b
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 04 10:52:41 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 04 10:52:41 2013 +0100
     1.3 @@ -159,8 +159,9 @@
     1.4            ||> (fn info => (SOME info, NONE))
     1.5          else
     1.6            derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
     1.7 -            dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
     1.8 -            ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
     1.9 +            dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
    1.10 +            ctr_defss ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy)
    1.11 +            lthy
    1.12            |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
    1.13                    (disc_unfold_thmss, disc_corec_thmss, _), _,
    1.14                    (sel_unfold_thmsss, sel_corec_thmsss, _)) =>