src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 51805 67757f1d5e71
parent 51804 be6e703908f4
child 51808 355dcd6a9b3c
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 09:10:49 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 09:45:14 2013 +0200
     1.3 @@ -255,10 +255,10 @@
     1.4      val fp_eqs =
     1.5        map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsXs;
     1.6  
     1.7 -    (* TODO: clean up list *)
     1.8 -    val (pre_bnfs, ((fp_bnfs as any_fp_bnf :: _, dtors0, ctors0, fp_folds0, fp_recs0, fp_induct,
     1.9 -           fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects, fp_map_thms, fp_set_thmss,
    1.10 -           fp_rel_thms, fp_fold_thms, fp_rec_thms), lthy)) =
    1.11 +    val (pre_bnfs, ({bnfs = fp_bnfs as any_fp_bnf :: _, dtors = dtors0, ctors = ctors0,
    1.12 +           folds = fp_folds0, recs = fp_recs0, induct = fp_induct, strong_induct = fp_strong_induct,
    1.13 +           dtor_ctors, ctor_dtors, ctor_injects, map_thms = fp_map_thms, set_thmss = fp_set_thmss,
    1.14 +           rel_thms = fp_rel_thms, fold_thms = fp_fold_thms, rec_thms = fp_rec_thms}, lthy)) =
    1.15        fp_bnf construct_fp fp_bs mixfixes map_bs rel_bs set_bss (map dest_TFree unsorted_As) fp_eqs
    1.16          no_defs_lthy0;
    1.17