src/HOL/BNF/Tools/bnf_fp_util.ML
changeset 52312 f461dca57c66
parent 52207 21026c312cc3
child 52314 9606cf677021
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Jun 06 11:19:04 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Jun 06 11:33:41 2013 +0200
     1.3 @@ -15,18 +15,18 @@
     1.4       bnfs: BNF_Def.bnf list,
     1.5       ctors: term list,
     1.6       dtors: term list,
     1.7 -     un_folds: term list,
     1.8 -     co_recs: term list,
     1.9 -     co_induct: thm,
    1.10 -     strong_co_induct: thm,
    1.11 +     xtor_un_folds: term list,
    1.12 +     xtor_co_recs: term list,
    1.13 +     xtor_co_induct: thm,
    1.14 +     xtor_strong_co_induct: thm,
    1.15       dtor_ctors: thm list,
    1.16       ctor_dtors: thm list,
    1.17       ctor_injects: thm list,
    1.18       map_thms: thm list,
    1.19       set_thmss: thm list list,
    1.20       rel_thms: thm list,
    1.21 -     un_fold_thms: thm list,
    1.22 -     co_rec_thms: thm list}
    1.23 +     xtor_un_fold_thms: thm list,
    1.24 +     xtor_co_rec_thms: thm list}
    1.25  
    1.26    val morph_fp_result: morphism -> fp_result -> fp_result
    1.27    val eq_fp_result: fp_result * fp_result -> bool
    1.28 @@ -185,38 +185,38 @@
    1.29     bnfs: BNF_Def.bnf list,
    1.30     ctors: term list,
    1.31     dtors: term list,
    1.32 -   un_folds: term list,
    1.33 -   co_recs: term list,
    1.34 -   co_induct: thm,
    1.35 -   strong_co_induct: thm,
    1.36 +   xtor_un_folds: term list,
    1.37 +   xtor_co_recs: term list,
    1.38 +   xtor_co_induct: thm,
    1.39 +   xtor_strong_co_induct: thm,
    1.40     dtor_ctors: thm list,
    1.41     ctor_dtors: thm list,
    1.42     ctor_injects: thm list,
    1.43     map_thms: thm list,
    1.44     set_thmss: thm list list,
    1.45     rel_thms: thm list,
    1.46 -   un_fold_thms: thm list,
    1.47 -   co_rec_thms: thm list};
    1.48 +   xtor_un_fold_thms: thm list,
    1.49 +   xtor_co_rec_thms: thm list};
    1.50  
    1.51 -fun morph_fp_result phi {Ts, bnfs, ctors, dtors, un_folds, co_recs, co_induct, strong_co_induct,
    1.52 -    dtor_ctors, ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms, un_fold_thms,
    1.53 -    co_rec_thms} =
    1.54 +fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_un_folds, xtor_co_recs, xtor_co_induct,
    1.55 +    xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms,
    1.56 +    xtor_un_fold_thms, xtor_co_rec_thms} =
    1.57    {Ts = map (Morphism.typ phi) Ts,
    1.58     bnfs = map (morph_bnf phi) bnfs,
    1.59     ctors = map (Morphism.term phi) ctors,
    1.60     dtors = map (Morphism.term phi) dtors,
    1.61 -   un_folds = map (Morphism.term phi) un_folds,
    1.62 -   co_recs = map (Morphism.term phi) co_recs,
    1.63 -   co_induct = Morphism.thm phi co_induct,
    1.64 -   strong_co_induct = Morphism.thm phi strong_co_induct,
    1.65 +   xtor_un_folds = map (Morphism.term phi) xtor_un_folds,
    1.66 +   xtor_co_recs = map (Morphism.term phi) xtor_co_recs,
    1.67 +   xtor_co_induct = Morphism.thm phi xtor_co_induct,
    1.68 +   xtor_strong_co_induct = Morphism.thm phi xtor_strong_co_induct,
    1.69     dtor_ctors = map (Morphism.thm phi) dtor_ctors,
    1.70     ctor_dtors = map (Morphism.thm phi) ctor_dtors,
    1.71     ctor_injects = map (Morphism.thm phi) ctor_injects,
    1.72     map_thms = map (Morphism.thm phi) map_thms,
    1.73     set_thmss = map (map (Morphism.thm phi)) set_thmss,
    1.74     rel_thms = map (Morphism.thm phi) rel_thms,
    1.75 -   un_fold_thms = map (Morphism.thm phi) un_fold_thms,
    1.76 -   co_rec_thms = map (Morphism.thm phi) co_rec_thms};
    1.77 +   xtor_un_fold_thms = map (Morphism.thm phi) xtor_un_fold_thms,
    1.78 +   xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms};
    1.79  
    1.80  fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
    1.81    eq_list eq_bnf (bnfs1, bnfs2);