src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
changeset 53808 b3e2022530e3
parent 53746 bd038e48526d
child 53974 612505263257
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Sep 23 23:27:46 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Sep 24 00:01:10 2013 +0200
     1.3 @@ -157,7 +157,7 @@
     1.4            derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
     1.5              xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
     1.6              co_iterss co_iter_defss lthy
     1.7 -          |> `(fn ((_, induct, _), (fold_thmss, _), (rec_thmss, _)) =>
     1.8 +          |> `(fn ((_, induct, _), (fold_thmss, rec_thmss, _)) =>
     1.9              ([induct], fold_thmss, rec_thmss, [], [], [], []))
    1.10            ||> (fn info => (SOME info, NONE))
    1.11          else